OpenMath Content Dictionary: group1

Canonical URL:

http://www.openmath.org/cd/group1.ocd

CD Base:

http://www.openmath.org/cd

CD File:

group1.ocd

CD as XML Encoded OpenMath:

group1.omcd

Defines:

multiplication, carrier, expression, group, identity, inversion, is_commutative, is_normal, is_subgroup, monoid, normal_closure, power, subgroup

Date:

1999-05-10

Version:

3

Review Date:

2003-04-01

Status:

experimental

---

A CD of basic functions for group theory

Written by A. Solomon on 1998-11-19
Modified by David Carlisle 1998-04-28
Severely edited by Arjeh M. Cohen in 2003

---

group

Description:

This symbol is a constructor for groups. It takes four arguments in the following order: a set to specify the elements in the group, a binary operation to specify the group operation, an element to specify the identity, and a unary operation to specify inverses of group elements. Both the binary and unary operations should act on elements of the set and return an element of the set.

Commented Mathematical property (CMP):

A group is closed under its operation. A groups operation is associative. A group has an identity element. Every element of a group has an inverse.

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMV name="G"/>
      <OMA>
        <OMS cd="group1" name="group"/>
	<OMV name="set"/>
	<OMV name="binop"/>
	<OMV name="elt"/>
	<OMV name="unop"/>
      </OMA>
    </OMA>
    <OMA>
      <OMS cd="logic1" name="and"/>
      <OMA>
        <OMS cd="logic1" name="implies"/>
	<OMA>
	  <OMS cd="logic1" name="and"/>
	  <OMA>
	    <OMS cd="set1" name="in"/>
	    <OMV name="x"/>
	    <OMV name="set"/>
	  </OMA>
	  <OMA>
	    <OMS cd="set1" name="in"/>
	    <OMV name="y"/>
	    <OMV name="set"/>
	  </OMA>
	</OMA>
	<OMA>
	  <OMS cd="set1" name="in"/>
	  <OMA>
	    <OMV name="binop"/>
	    <OMV name="x"/>
	    <OMV name="y"/>
	  </OMA>
	  <OMV name="set"/>
	</OMA>
      </OMA>
      <OMA>
        <OMS cd="relation1" name="eq"/>
	<OMA>
	  <OMV name="binop"/>
	  <OMV name="x"/>
	  <OMA>
	    <OMV name="binop"/>
	    <OMV name="y"/>
	    <OMV name="z"/>
	  </OMA>
	</OMA>
	<OMA>
	  <OMV name="binop"/>
	  <OMA>
	    <OMV name="binop"/>
	    <OMV name="x"/>
	    <OMV name="y"/>
	  </OMA>
	  <OMV name="z"/>
	</OMA>
      </OMA>
      <OMA>
        <OMS cd="logic1" name="and"/>
	<OMA>
	  <OMS cd="set1" name="in"/>
	  <OMV name="elt"/>
	  <OMV name="set"/>
	</OMA>
	<OMBIND>
	  <OMS cd="quant1" name="forall"/>
	  <OMBVAR>
	    <OMV name="x"/>
	  </OMBVAR>
	  <OMA>
	    <OMS cd="logic1" name="implies"/>
	    <OMA>
	      <OMS cd="set1" name="in"/>
	      <OMV name="x"/>
	      <OMV name="set"/>
	    </OMA>
	    <OMA>
	      <OMS cd="logic1" name="and"/>
	      <OMA>
	        <OMS cd="relation1" name="eq"/>
		<OMA>
		  <OMV name="binop"/>
		  <OMV name="elt"/>
		  <OMV name="x"/>
		</OMA>
		<OMV name="x"/>
	      </OMA>
	      <OMA>
	        <OMS cd="relation1" name="eq"/>
		<OMA>
		  <OMV name="binop"/>
		  <OMV name="x"/>
		  <OMV name="elt"/>
		</OMA>
		<OMV name="x"/>
	      </OMA>
	    </OMA>
	  </OMA>
	</OMBIND>
      </OMA>
      <OMBIND>
        <OMS cd="quant1" name="forall"/>
	<OMBVAR>
	  <OMV name="x"/>
	</OMBVAR>
	<OMA>
	  <OMS cd="logic1" name="implies"/>
	  <OMA>
	    <OMS cd="set1" name="in"/>
	    <OMV name="x"/>
	    <OMV name="set"/>
	  </OMA>
	  <OMA>
	    <OMS cd="relation1" name="eq"/>
	    <OMA>
	      <OMV name="binop"/>
	      <OMV name="x"/>
	      <OMA>
	        <OMV name="unop"/>
		<OMV name="x"/>
	      </OMA>
	    </OMA>
	    <OMV name="elt"/>
	  </OMA>
	</OMA>
      </OMBIND>
    </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="relation1">eq</csymbol>
   <ci>G</ci>
   <apply><csymbol cd="group1">group</csymbol>
    <ci>set</ci>
    <ci>binop</ci>
    <ci>elt</ci>
    <ci>unop</ci>
   </apply>
  </apply>
  <apply><csymbol cd="logic1">and</csymbol>
   <apply><csymbol cd="logic1">implies</csymbol>
    <apply><csymbol cd="logic1">and</csymbol>
     <apply><csymbol cd="set1">in</csymbol><ci>x</ci><ci>set</ci></apply>
     <apply><csymbol cd="set1">in</csymbol><ci>y</ci><ci>set</ci></apply>
    </apply>
    <apply><csymbol cd="set1">in</csymbol>
     <apply><ci>binop</ci><ci>x</ci><ci>y</ci></apply>
     <ci>set</ci>
    </apply>
   </apply>
   <apply><csymbol cd="relation1">eq</csymbol>
    <apply>
     <ci>binop</ci>
     <ci>x</ci>
     <apply><ci>binop</ci><ci>y</ci><ci>z</ci></apply>
    </apply>
    <apply>
     <ci>binop</ci>
     <apply><ci>binop</ci><ci>x</ci><ci>y</ci></apply>
     <ci>z</ci>
    </apply>
   </apply>
   <apply><csymbol cd="logic1">and</csymbol>
    <apply><csymbol cd="set1">in</csymbol><ci>elt</ci><ci>set</ci></apply>
    <bind><csymbol cd="quant1">forall</csymbol>
     <bvar><ci>x</ci></bvar>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><csymbol cd="set1">in</csymbol><ci>x</ci><ci>set</ci></apply>
      <apply><csymbol cd="logic1">and</csymbol>
       <apply><csymbol cd="relation1">eq</csymbol>
        <apply><ci>binop</ci><ci>elt</ci><ci>x</ci></apply>
        <ci>x</ci>
       </apply>
       <apply><csymbol cd="relation1">eq</csymbol>
        <apply><ci>binop</ci><ci>x</ci><ci>elt</ci></apply>
        <ci>x</ci>
       </apply>
      </apply>
     </apply>
    </bind>
   </apply>
   <bind><csymbol cd="quant1">forall</csymbol>
    <bvar><ci>x</ci></bvar>
    <apply><csymbol cd="logic1">implies</csymbol>
     <apply><csymbol cd="set1">in</csymbol><ci>x</ci><ci>set</ci></apply>
     <apply><csymbol cd="relation1">eq</csymbol>
      <apply><ci>binop</ci><ci>x</ci><apply><ci>unop</ci><ci>x</ci></apply></apply>
      <ci>elt</ci>
     </apply>
    </apply>
   </bind>
  </apply>
 </apply>
</math>

Prefix

implies (eq ( G, group ( set, binop, elt, unop) ) , and (implies (and (in ( x, set) , in ( y, set) ) , in ( binop ( x, y) , set) ) , eq ( binop ( x, binop ( y, z) ) , binop ( binop ( x, y) , z) ) , and (in ( elt, set) , forall [ x ] . (implies (in ( x, set) , and (eq ( binop ( elt, x) , x) , eq ( binop ( x, elt) , x) ) ) ) ) , forall [ x ] . (implies (in ( x, set) , eq ( binop ( x, unop ( x) ) , elt) ) ) ) )

Popcorn

$G = group1.group($set, $binop, $elt, $unop) ==> (set1.in($x, $set) and set1.in($y, $set) ==> set1.in($binop($x, $y), $set)) and $binop($x, $binop($y, $z)) = $binop($binop($x, $y), $z) and set1.in($elt, $set) and quant1.forall[$x -> set1.in($x, $set) ==> $binop($elt, $x) = $x and $binop($x, $elt) = $x] and quant1.forall[$x -> set1.in($x, $set) ==> $binop($x, $unop($x)) = $elt]

Rendered Presentation MathML

$$G=\mathrm{group}(\mathrm{set},\mathrm{binop},\mathrm{elt},\mathrm{unop})\Rightarrow (x\in \mathrm{set}\wedge y\in \mathrm{set}\Rightarrow \mathrm{binop}(x,y)\in \mathrm{set})\wedge \mathrm{binop}(x,\mathrm{binop}(y,z))=\mathrm{binop}(\mathrm{binop}(x,y),z)\wedge \mathrm{elt}\in \mathrm{set}\wedge \forall \hspace{0.17em}x.x\in \mathrm{set}\Rightarrow \mathrm{binop}(\mathrm{elt},x)=x\wedge \mathrm{binop}(x,\mathrm{elt})=x\wedge \forall \hspace{0.17em}x.x\in \mathrm{set}\Rightarrow \mathrm{binop}(x,\mathrm{unop}\left(x\right))=\mathrm{elt}$$

Example:

This example represents the group which has as elements all positive and negative even numbers, the group operation is binary addition, inverses are the negative of the element and the identity is the zero element.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA>
  <OMS cd="group1" name="group"/>
  <OMA>
    <OMS cd="set1" name="suchthat"/>
    <OMS cd="setname1" name="Z"/>
    <OMBIND>
      <OMS cd="fns1" name="lambda"/>
      <OMBVAR>
        <OMV name="x"/>
      </OMBVAR>
      <OMA>
        <OMS cd="set1" name="in"/>
        <OMA>
          <OMS cd="arith1" name="divide"/>
          <OMV name="x"/>
          <OMI> 2 </OMI>
        </OMA>
        <OMS cd="setname1" name="Z"/>
      </OMA>
    </OMBIND>
  </OMA>
  <OMS cd="arith1" name="plus"/>
  <OMS cd="alg1" name="zero"/>
  <OMS cd="arith1" name="unary_minus"/>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="group1">group</csymbol>
  <apply><csymbol cd="set1">suchthat</csymbol>
   <csymbol cd="setname1">Z</csymbol>
   <bind><csymbol cd="fns1">lambda</csymbol>
    <bvar><ci>x</ci></bvar>
    <apply><csymbol cd="set1">in</csymbol>
     <apply><csymbol cd="arith1">divide</csymbol><ci>x</ci><cn type="integer">2</cn></apply>
     <csymbol cd="setname1">Z</csymbol>
    </apply>
   </bind>
  </apply>
  <csymbol cd="arith1">plus</csymbol>
  <csymbol cd="alg1">zero</csymbol>
  <csymbol cd="arith1">unary_minus</csymbol>
 </apply>
</math>

Prefix

group (suchthat (Z, lambda [ x ] . (in (divide ( x, 2 ) , Z) ) ) , plus, zero, unary_minus)

Popcorn

group1.group(set1.suchthat(setname1.Z, fns1.lambda[$x -> set1.in($x / 2, setname1.Z)]), arith1.plus, alg1.zero, arith1.unary_minus)

Rendered Presentation MathML

$$\mathrm{group}(\left\{x\in \mathbb{Z}\right|\frac{x}{2}\in \mathbb{Z}\},+,0,-)$$

Signatures:

sts

---

[Next: carrier] [Last: is_normal] [Top]

---

carrier

Description:

This symbol represents a unary function, whose argument should be a group G (for instance constructed by group). When applied to G, its value should be the set of elements of G.

Example:

The carrier of group(G,*,e,inverse) is G.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="group1" name="carrier"/>
            <OMA><OMS cd="group1" name="group"/>
                 <OMV name="G"/>
                 <OMV name="times"/>
                 <OMV name="e"/>
                 <OMV name="inverse"/>
            </OMA>
       </OMA>
       <OMV name="G"/>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="group1">carrier</csymbol>
   <apply><csymbol cd="group1">group</csymbol>
    <ci>G</ci>
    <ci>times</ci>
    <ci>e</ci>
    <ci>inverse</ci>
   </apply>
  </apply>
  <ci>G</ci>
 </apply>
</math>

Prefix

eq (carrier (group ( G, times, e, inverse) ) , G)

Popcorn

group1.carrier(group1.group($G, $times, $e, $inverse)) = $G

Rendered Presentation MathML

$$\mathrm{carrier}\left(\mathrm{group}(G,\mathrm{times},e,\mathrm{inverse})\right)=G$$

Signatures:

sts

---

[Next: multiplication] [Previous: group] [Top]

---

multiplication

Description:

This symbol represents a unary function, whose argument should be a group G. It returns the multiplication map on G. We allow for the map to be n-ary.

Example:

The multiplication of group(G,*,inverse,e) is *.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="group1" name="multiplication"/>
            <OMA><OMS cd="group1" name="group"/>
                 <OMV name="G"/>
                 <OMV name="times"/>
                 <OMV name="e"/>
                 <OMV name="inverse"/>
            </OMA>
       </OMA>
       <OMV name="times"/>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="group1">multiplication</csymbol>
   <apply><csymbol cd="group1">group</csymbol>
    <ci>G</ci>
    <ci>times</ci>
    <ci>e</ci>
    <ci>inverse</ci>
   </apply>
  </apply>
  <ci>times</ci>
 </apply>
</math>

Prefix

eq (multiplication (group ( G, times, e, inverse) ) , times)

Popcorn

group1.multiplication(group1.group($G, $times, $e, $inverse)) = $times

Rendered Presentation MathML

$$\mathrm{multiplication}\left(\mathrm{group}(G,\mathrm{times},e,\mathrm{inverse})\right)=\mathrm{times}$$

Signatures:

sts

---

[Next: inversion] [Previous: carrier] [Top]

---

inversion

Description:

This symbol represents a unary function, whose argument should be a group G. It returns the map sending an element of G to its inverse.

Example:

The inversion of group(G,*,e,inverse) is inverse.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="group1" name="inversion"/>
            <OMA><OMS cd="group1" name="group"/>
                 <OMV name="G"/>
                 <OMV name="times"/>
                 <OMV name="e"/>
                 <OMV name="inverse"/>
            </OMA>
       </OMA>
       <OMV name="inverse"/>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="group1">inversion</csymbol>
   <apply><csymbol cd="group1">group</csymbol>
    <ci>G</ci>
    <ci>times</ci>
    <ci>e</ci>
    <ci>inverse</ci>
   </apply>
  </apply>
  <ci>inverse</ci>
 </apply>
</math>

Prefix

eq (inversion (group ( G, times, e, inverse) ) , inverse)

Popcorn

group1.inversion(group1.group($G, $times, $e, $inverse)) = $inverse

Rendered Presentation MathML

$$\mathrm{inversion}\left(\mathrm{group}(G,\mathrm{times},e,\mathrm{inverse})\right)=\mathrm{inverse}$$

Signatures:

sts

---

[Next: identity] [Previous: multiplication] [Top]

---

identity

Description:

This symbols represents a unary function, whose argument should be a group. It returns the identity element of the group.

Example:

The identity of group(G,*,e,inverse) is e.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="group1" name="identity"/>
            <OMA><OMS cd="group1" name="group"/>
                 <OMV name="G"/>
                 <OMV name="times"/>
                 <OMV name="e"/>
                 <OMV name="inverse"/>
            </OMA>
       </OMA>
       <OMV name="e"/>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="group1">identity</csymbol>
   <apply><csymbol cd="group1">group</csymbol>
    <ci>G</ci>
    <ci>times</ci>
    <ci>e</ci>
    <ci>inverse</ci>
   </apply>
  </apply>
  <ci>e</ci>
 </apply>
</math>

Prefix

eq (identity (group ( G, times, e, inverse) ) , e)

Popcorn

group1.identity(group1.group($G, $times, $e, $inverse)) = $e

Rendered Presentation MathML

$$\mathrm{identity}\left(\mathrm{group}(G,\mathrm{times},e,\mathrm{inverse})\right)=e$$

Signatures:

sts

---

[Next: is_commutative] [Previous: inversion] [Top]

---

is_commutative

Description:

The unary boolean function whose value is true iff the argument is a commutative group.

Commented Mathematical property (CMP):

If is_commutative(G) then for all a,b in carrier(G) a*b = b*a

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="group1" name="is_commutative"/>
      <OMV name="G"/>
    </OMA>
    <OMBIND>
      <OMS cd="quant1" name="forall"/>
      <OMBVAR>
        <OMV name="a"/>
        <OMV name="b"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="implies"/>
        <OMA>
          <OMS cd="logic1" name="and"/>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMV name="a"/>
            <OMA>
              <OMS cd="group1" name="carrier"/>
              <OMV name="G"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMV name="b"/>
            <OMA>
              <OMS cd="group1" name="carrier"/>
              <OMV name="G"/>
            </OMA>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
            <OMA>
              <OMS cd="group1" name="multiplication"/>
              <OMV name="G"/>
            </OMA>
            <OMV name="a"/>
            <OMV name="b"/>
          </OMA>
          <OMA>
            <OMA>
              <OMS cd="group1" name="multiplication"/>
              <OMV name="G"/>
            </OMA>
            <OMV name="b"/>
            <OMV name="a"/>
          </OMA>
        </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="group1">is_commutative</csymbol><ci>G</ci></apply>
  <bind><csymbol cd="quant1">forall</csymbol>
   <bvar><ci>a</ci></bvar>
   <bvar><ci>b</ci></bvar>
   <apply><csymbol cd="logic1">implies</csymbol>
    <apply><csymbol cd="logic1">and</csymbol>
     <apply><csymbol cd="set1">in</csymbol>
      <ci>a</ci>
      <apply><csymbol cd="group1">carrier</csymbol><ci>G</ci></apply>
     </apply>
     <apply><csymbol cd="set1">in</csymbol>
      <ci>b</ci>
      <apply><csymbol cd="group1">carrier</csymbol><ci>G</ci></apply>
     </apply>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply><csymbol cd="group1">multiplication</csymbol><ci>G</ci></apply>
     <ci>a</ci>
     <ci>b</ci>
    </apply>
    <apply>
     <apply><csymbol cd="group1">multiplication</csymbol><ci>G</ci></apply>
     <ci>b</ci>
     <ci>a</ci>
    </apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

implies (is_commutative ( G) , forall [ a b ] . (implies (and (in ( a, carrier ( G) ) , in ( b, carrier ( G) ) ) , eq (multiplication ( G) , a, b) , multiplication ( G) ( b, a) ) ) )

Popcorn

group1.is_commutative($G) ==> quant1.forall[$a, $b -> set1.in($a, group1.carrier($G)) and set1.in($b, group1.carrier($G)) ==> group1.multiplication($G) = $a = $b ==> group1.multiplication($G)($b, $a)]

Rendered Presentation MathML

$$\mathrm{is\_commutative}\left(G\right)\Rightarrow \forall \hspace{0.17em}a,b.a\in \mathrm{carrier}\left(G\right)\wedge b\in \mathrm{carrier}\left(G\right)\Rightarrow \mathrm{multiplication}\left(G\right)=a=b$$

Signatures:

sts

---

[Next: is_subgroup] [Previous: identity] [Top]

---

is_subgroup

Description:

The binary boolean function whose value is true iff the second argument is a subgroup of the second.

Commented Mathematical property (CMP):

If is_subgroup(G,H) then H is a nonempty set of elements of G and H is closed under multiplication and taking inverses.

Signatures:

sts

---

[Next: monoid] [Previous: is_commutative] [Top]

---

monoid

Description:

This symbol is a unary function, whose argument should be a group G. When applied to G its value is the monoid underlying G.

Example:

OpenMath XML (source)

    <OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
     <OMA><OMS cd="group1" name="monoid"/>
          <OMV name="G"/> 
     </OMA>
    </OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML"><apply><csymbol cd="group1">monoid</csymbol><ci>G</ci></apply></math>

Prefix

monoid ( G)

Popcorn

group1.monoid($G)

Rendered Presentation MathML

$$\mathrm{monoid}\left(G\right)$$

Signatures:

sts

---

[Next: subgroup] [Previous: is_subgroup] [Top]

---

subgroup

Description:

This symbol is a constructor symbol with one or two arguments. The first argument is a list or set, D, of group elements. The optional second argument is the group G containing D. It denotes the subgroup of G generated by D.

Example:

OpenMath XML (source)

    <OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
     <OMA><OMS cd="group1" name="subgroup"/>
          <OMV name="D"/> <OMV name="G"/>
     </OMA>
    </OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML"><apply><csymbol cd="group1">subgroup</csymbol><ci>D</ci><ci>G</ci></apply></math>

Prefix

subgroup ( D, G)

Popcorn

group1.subgroup($D, $G)

Rendered Presentation MathML

$$\mathrm{subgroup}(D,G)$$

Example:

This example represents the subgroup of the multiplicative group of the nonzero reals generated by the constants Pi and E:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="group1" name="subgroup"/>
     <OMA>
       <OMS cd="list1" name="list"/>
         <OMS cd="nums1" name="pi"/>
         <OMS cd="nums1" name="e"/>
     </OMA>
     <OMA><OMS cd="group1" name="group"/>
          <OMA><OMS cd="set1" name="suchthat"/>
               <OMS cd="setname1" name="R"/>
               <OMBIND><OMS cd="fns1" name="lambda"/>
                       <OMBVAR> <OMV name="x"/>
                       </OMBVAR>
                       <OMA><OMS cd="relation1" name="neq"/>
                            <OMV name="x"/>
                            <OMS cd="alg1" name="zero"/>
                       </OMA>
               </OMBIND>
          </OMA>
          <OMS cd="arith1" name="times"/>
          <OMI> 1 </OMI>
          <OMS cd="arith2" name="inverse"/>
     </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="group1">subgroup</csymbol>
  <apply><csymbol cd="list1">list</csymbol>
   <csymbol cd="nums1">pi</csymbol>
   <csymbol cd="nums1">e</csymbol>
  </apply>
  <apply><csymbol cd="group1">group</csymbol>
   <apply><csymbol cd="set1">suchthat</csymbol>
    <csymbol cd="setname1">R</csymbol>
    <bind><csymbol cd="fns1">lambda</csymbol>
     <bvar><ci>x</ci></bvar>
     <apply><csymbol cd="relation1">neq</csymbol><ci>x</ci><csymbol cd="alg1">zero</csymbol></apply>
    </bind>
   </apply>
   <csymbol cd="arith1">times</csymbol>
   <cn type="integer">1</cn>
   <csymbol cd="arith2">inverse</csymbol>
  </apply>
 </apply>
</math>

Prefix

subgroup (list (pi, e) , group (suchthat (R, lambda [ x ] . (neq ( x, zero) ) ) , times, 1 , inverse) )

Popcorn

group1.subgroup([nums1.pi , nums1.e], group1.group(set1.suchthat(setname1.R, fns1.lambda[$x -> $x != alg1.zero]), arith1.times, 1, arith2.inverse))

Rendered Presentation MathML

$$\mathrm{subgroup}((\pi ,e),\mathrm{group}(\left\{x\in \mathbb{R}\right|x\ne 0\},\times ,1,\mathrm{inverse}))$$

Signatures:

sts

---

[Next: power] [Previous: monoid] [Top]

---

power

Description:

This is a symbol with three arguments. The first argument is a group G. Its second argument is an element g of G and the third argument is an integer k. It denotes the element g^k in G.

Example:

OpenMath XML (source)

  <OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
    <OMA><OMS cd="relation1" name="eq"/>
        <OMA><OMS cd="group1" name="power"/>
            <OMA><OMS cd="group1" name="group"/>
                <OMS cd="setname1" name="Z"/>
                <OMS cd="arith1" name="plus"/>
                <OMI>0</OMI>
                <OMS cd="arith1" name="unary_minus"/>
            </OMA>
            <OMI>3</OMI>
            <OMI>2</OMI>
        </OMA>
        <OMI>6</OMI>
    </OMA>
  </OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="group1">power</csymbol>
   <apply><csymbol cd="group1">group</csymbol>
    <csymbol cd="setname1">Z</csymbol>
    <csymbol cd="arith1">plus</csymbol>
    <cn type="integer">0</cn>
    <csymbol cd="arith1">unary_minus</csymbol>
   </apply>
   <cn type="integer">3</cn>
   <cn type="integer">2</cn>
  </apply>
  <cn type="integer">6</cn>
 </apply>
</math>

Prefix

eq (power (group (Z, plus, 0, unary_minus) , 3, 2) , 6)

Popcorn

group1.power(group1.group(setname1.Z, arith1.plus, 0, arith1.unary_minus), 3, 2) = 6

Rendered Presentation MathML

$$\mathrm{power}(\mathrm{group}(\mathbb{Z},+,0,-),3,2)=6$$

Signatures:

sts

---

[Next: expression] [Previous: subgroup] [Top]

---

expression

Description:

This symbol is a function with two arguments. Its first argument should be a group. The second should be an arithmetic expression A, whose operators are times and power, and whose leaves are members of the carrier of G. When applied to G and A, it denotes the element (of G) that is obtained from the leaves of A by applying the multiplication and the power map of G instead of the times and power from the CD arith1 appearing in A. The symbol alg1.one occurring in A will be interpreted as the identity of G.

Example:

OpenMath XML (source)

  <OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
    <OMA><OMS cd="relation1" name="eq"/>
         <OMA><OMS cd="group1" name="expression"/>
              <OMA><OMS cd="group1" name="group"/>
                   <OMS cd="setname1" name="Z"/>
                   <OMS cd="arith1" name="plus"/>
                   <OMI>0</OMI>
                   <OMS cd="arith1" name="unary_minus"/>
              </OMA>
              <OMA><OMS cd="arith1" name="times"/>
                   <OMI>6</OMI><OMI>3</OMI>
              </OMA>
         </OMA>
         <OMI>9</OMI>
    </OMA>
  </OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="group1">expression</csymbol>
   <apply><csymbol cd="group1">group</csymbol>
    <csymbol cd="setname1">Z</csymbol>
    <csymbol cd="arith1">plus</csymbol>
    <cn type="integer">0</cn>
    <csymbol cd="arith1">unary_minus</csymbol>
   </apply>
   <apply><csymbol cd="arith1">times</csymbol>
    <cn type="integer">6</cn>
    <cn type="integer">3</cn>
   </apply>
  </apply>
  <cn type="integer">9</cn>
 </apply>
</math>

Prefix

eq (expression (group (Z, plus, 0, unary_minus) , times (6, 3) ) , 9)

Popcorn

group1.expression(group1.group(setname1.Z, arith1.plus, 0, arith1.unary_minus), 6 * 3) = 9

Rendered Presentation MathML

$$\mathrm{expression}(\mathrm{group}(\mathbb{Z},+,0,-),6\times 3)=9$$

Signatures:

sts

---

[Next: normal_closure] [Previous: power] [Top]

---

normal_closure

Description:

The binary function whose value is the set of conjugates of the elements of the second group by elements of the first, where multiplication between them is defined.

Commented Mathematical property (CMP):

n in the normal closure (A,B) implies there exists a in A and b in B s.t. n = b^(-1) a b

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="set1" name="in"/>
      <OMV name="n"/>
      <OMA>
        <OMS cd="group1" name="normal_closure"/>
	<OMV name="A"/>
	<OMV name="B"/>
      </OMA>
    </OMA>
    <OMBIND>
      <OMS cd="quant1" name="exists"/>
      <OMBVAR>
        <OMV name="a"/>
	<OMV name="b"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="and"/>
	<OMA>
	  <OMS cd="set1" name="in"/>
	  <OMV name="a"/>
	  <OMA>
	    <OMS cd="group1" name="carrier"/>
	    <OMV name="A"/>
	  </OMA>
	</OMA>
	<OMA>
	  <OMS cd="set1" name="in"/>
	  <OMV name="b"/>
	  <OMA>
	    <OMS cd="group1" name="carrier"/>
	    <OMV name="B"/>
	  </OMA>
	</OMA>
	<OMA>
	  <OMS cd="relation1" name="eq"/>
	  <OMV name="n"/>
	  <OMA>
	    <OMS cd="arith1" name="times"/>
	    <OMV name="invb"/>
	    <OMV name="a"/>
	    <OMV name="b"/>
	  </OMA>
	</OMA>
	<OMA>
	  <OMS cd="relation1" name="eq"/>
	  <OMA>
	    <OMS cd="arith1" name="times"/>
	    <OMV name="invb"/>
	    <OMV name="b"/>
	  </OMA>
	  <OMS cd="alg1" name="one"/>
	</OMA>
      </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="set1">in</csymbol>
   <ci>n</ci>
   <apply><csymbol cd="group1">normal_closure</csymbol><ci>A</ci><ci>B</ci></apply>
  </apply>
  <bind><csymbol cd="quant1">exists</csymbol>
   <bvar><ci>a</ci></bvar>
   <bvar><ci>b</ci></bvar>
   <apply><csymbol cd="logic1">and</csymbol>
    <apply><csymbol cd="set1">in</csymbol>
     <ci>a</ci>
     <apply><csymbol cd="group1">carrier</csymbol><ci>A</ci></apply>
    </apply>
    <apply><csymbol cd="set1">in</csymbol>
     <ci>b</ci>
     <apply><csymbol cd="group1">carrier</csymbol><ci>B</ci></apply>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <ci>n</ci>
     <apply><csymbol cd="arith1">times</csymbol><ci>invb</ci><ci>a</ci><ci>b</ci></apply>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply><csymbol cd="arith1">times</csymbol><ci>invb</ci><ci>b</ci></apply>
     <csymbol cd="alg1">one</csymbol>
    </apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

implies (in ( n, normal_closure ( A, B) ) , exists [ a b ] . (and (in ( a, carrier ( A) ) , in ( b, carrier ( B) ) , eq ( n, times ( invb, a, b) ) , eq (times ( invb, b) , one) ) ) )

Popcorn

set1.in($n, group1.normal_closure($A, $B)) ==> quant1.exists[$a, $b -> set1.in($a, group1.carrier($A)) and set1.in($b, group1.carrier($B)) and $n = $invb * $a * $b and $invb * $b = alg1.one]

Rendered Presentation MathML

$$n\in \mathrm{normal\_closure}(A,B)\Rightarrow \exists \hspace{0.17em}a,b.a\in \mathrm{carrier}\left(A\right)\wedge b\in \mathrm{carrier}\left(B\right)\wedge n=\mathrm{invb}ab\wedge \mathrm{invb}b=1$$

Signatures:

sts

---

[Next: is_normal] [Previous: expression] [Top]

---

is_normal

Description:

If G, H are the group arguments, then IsNormal(G,H) returns true precisely when H is normal in G. That is, inverse(g)*h*g is defined and contained in H for all h in H and g in G.

Commented Mathematical property (CMP):

is_normal(G,H) implies that for all g in G and h in H then inverse(g)*h*g is in H.

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="group1" name="is_normal"/>
      <OMV name="G"/>
      <OMV name="H"/>
    </OMA>
    <OMBIND>
      <OMS cd="quant1" name="forall"/>
      <OMBVAR>
        <OMV name="g"/>
        <OMV name="h"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="and"/>
        <OMA>
          <OMS cd="set1" name="in"/>
	  <OMV name="g"/>
	  <OMA>
	    <OMS cd="group1" name="carrier"/>
	    <OMV name="G"/>
	  </OMA>
        </OMA>
        <OMA>
          <OMS cd="set1" name="in"/>
	  <OMV name="h"/>
	  <OMA>
	    <OMS cd="group1" name="carrier"/>
	    <OMV name="H"/>
	  </OMA>
        </OMA>
        <OMA>
          <OMS cd="set1" name="in"/>
	  <OMA>
	    <OMS cd="arith1" name="times"/>
	    <OMV name="invg"/>
	    <OMV name="h"/>
	    <OMV name="g"/>
	  </OMA>
	  <OMA>
	    <OMS cd="group1" name="carrier"/>
	    <OMV name="H"/>
	  </OMA>
	  <OMA>
	    <OMS cd="arith1" name="times"/>
	    <OMV name="invg"/>
	    <OMV name="g"/>
	  </OMA>
        </OMA>
      </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="group1">is_normal</csymbol><ci>G</ci><ci>H</ci></apply>
  <bind><csymbol cd="quant1">forall</csymbol>
   <bvar><ci>g</ci></bvar>
   <bvar><ci>h</ci></bvar>
   <apply><csymbol cd="logic1">and</csymbol>
    <apply><csymbol cd="set1">in</csymbol>
     <ci>g</ci>
     <apply><csymbol cd="group1">carrier</csymbol><ci>G</ci></apply>
    </apply>
    <apply><csymbol cd="set1">in</csymbol>
     <ci>h</ci>
     <apply><csymbol cd="group1">carrier</csymbol><ci>H</ci></apply>
    </apply>
    <apply><csymbol cd="set1">in</csymbol>
     <apply><csymbol cd="arith1">times</csymbol><ci>invg</ci><ci>h</ci><ci>g</ci></apply>
     <apply><csymbol cd="group1">carrier</csymbol><ci>H</ci></apply>
     <apply><csymbol cd="arith1">times</csymbol><ci>invg</ci><ci>g</ci></apply>
    </apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

implies (is_normal ( G, H) , forall [ g h ] . (and (in ( g, carrier ( G) ) , in ( h, carrier ( H) ) , in (times ( invg, h, g) , carrier ( H) , times ( invg, g) ) ) ) )

Popcorn

group1.is_normal($G, $H) ==> quant1.forall[$g, $h -> set1.in($g, group1.carrier($G)) and set1.in($h, group1.carrier($H)) and set1.in($invg * $h * $g, group1.carrier($H), $invg * $g)]

Rendered Presentation MathML

$$\mathrm{is\_normal}(G,H)\Rightarrow \forall \hspace{0.17em}g,h.g\in \mathrm{carrier}\left(G\right)\wedge h\in \mathrm{carrier}\left(H\right)\wedge \mathrm{invg}hg\in \mathrm{carrier}\left(H\right)$$

Signatures:

sts

---

[First: group] [Previous: normal_closure] [Top]