OpenMath Content Dictionary: ring1

Canonical URL:

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

CD File:

ring1.ocd

CD as XML Encoded OpenMath:

ring1.omcd

Defines:

addition, additive_group, carrier, identity, is_commutative, is_subring, multiplication, multiplicative_monoid, negation, ring, subring, subtraction, zero, expression, power

Date:

2004-06-01

Version:

1 (Revision 1)

Review Date:

2006-06-01

Status:

experimental

A CD of basic functions for ring theory

Written by Arjeh M. Cohen 2004-02-25

ring

Description:

This symbol is a constructor for rings. It takes six arguments R, a, o, i, m, e,: which are, respectively, a set R to specify the elements in the ring, a binary operation a on R, an element o of R, and a unary operation i on R such that [R,a,o,i] is a commutative group, a binary operation m on R and an element e of R such that [R,m,e] is a monoid.

Commented Mathematical property (CMP):

The distributive laws m(x,a(y,z)) = a(m(x,y),m(x,z)) and m(a(y,z),x) = a(m(y,x),m(z,x)), where x,y,z are elements of R, should hold.

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="S"/>
           <OMA><OMS cd="ring1" name="ring"/>
                <OMV name="R"/>
                <OMV name="add"/>
                <OMV name="zero"/>
                <OMV name="minus"/>
                <OMV name="mult"/>
                <OMV name="unit"/>
           </OMA>
           <OMBIND><OMS cd="quant1" name="forall"/>
                <OMBVAR><OMV name="x"/><OMV name="y"/><OMV name="z"/>
                </OMBVAR>
                <OMA><OMS cd="logic1" name="implies"/>
                     <OMA><OMS cd="logic1" name="and"/>
                          <OMA><OMS cd="set1" name="in"/>
                               <OMV name="x"/><OMV name="R"/>
                          </OMA>
                          <OMA><OMS cd="set1" name="in"/>
                               <OMV name="y"/><OMV name="R"/>
                          </OMA>
                          <OMA><OMS cd="set1" name="in"/>
                               <OMV name="z"/><OMV name="R"/>
                          </OMA>
                     </OMA>
                     <OMA><OMS cd="logic1" name="and"/>
                          <OMA><OMS cd="relation1" name="eq"/>
                               <OMA><OMV name="mult"/>
                                    <OMV name="x"/>
                                    <OMA><OMV name="add"/>
                                         <OMV name="y"/><OMV name="z"/>
                                    </OMA>
                               </OMA>
                               <OMA><OMV name="add"/>
                                    <OMA><OMV name="mult"/>
                                         <OMV name="x"/> <OMV name="y"/>
                                    </OMA>
                                    <OMA><OMV name="mult"/>
                                         <OMV name="x"/><OMV name="z"/>
                                    </OMA>
                               </OMA>
                          </OMA>
                          <OMA><OMS cd="relation1" name="eq"/>
                               <OMA><OMV name="mult"/>
                                    <OMA><OMV name="add"/>
                                         <OMV name="y"/><OMV name="z"/>
                                    </OMA>
                                    <OMV name="x"/>
                               </OMA>
                               <OMA><OMV name="add"/>
                                    <OMA><OMV name="mult"/>
                                         <OMV name="y"/> <OMV name="x"/>
                                    </OMA>
                                    <OMA><OMV name="mult"/>
                                         <OMV name="z"/><OMV name="x"/>
                                    </OMA>
                               </OMA>
                          </OMA>
                     </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>S</ci>
   <apply><csymbol cd="ring1">ring</csymbol>
    <ci>R</ci>
    <ci>add</ci>
    <ci>zero</ci>
    <ci>minus</ci>
    <ci>mult</ci>
    <ci>unit</ci>
   </apply>
   <bind><csymbol cd="quant1">forall</csymbol>
    <bvar><ci>x</ci></bvar>
    <bvar><ci>y</ci></bvar>
    <bvar><ci>z</ci></bvar>
    <apply><csymbol cd="logic1">implies</csymbol>
     <apply><csymbol cd="logic1">and</csymbol>
      <apply><csymbol cd="set1">in</csymbol><ci>x</ci><ci>R</ci></apply>
      <apply><csymbol cd="set1">in</csymbol><ci>y</ci><ci>R</ci></apply>
      <apply><csymbol cd="set1">in</csymbol><ci>z</ci><ci>R</ci></apply>
     </apply>
     <apply><csymbol cd="logic1">and</csymbol>
      <apply><csymbol cd="relation1">eq</csymbol>
       <apply>
        <ci>mult</ci>
        <ci>x</ci>
        <apply><ci>add</ci><ci>y</ci><ci>z</ci></apply>
       </apply>
       <apply>
        <ci>add</ci>
        <apply><ci>mult</ci><ci>x</ci><ci>y</ci></apply>
        <apply><ci>mult</ci><ci>x</ci><ci>z</ci></apply>
       </apply>
      </apply>
      <apply><csymbol cd="relation1">eq</csymbol>
       <apply>
        <ci>mult</ci>
        <apply><ci>add</ci><ci>y</ci><ci>z</ci></apply>
        <ci>x</ci>
       </apply>
       <apply>
        <ci>add</ci>
        <apply><ci>mult</ci><ci>y</ci><ci>x</ci></apply>
        <apply><ci>mult</ci><ci>z</ci><ci>x</ci></apply>
       </apply>
      </apply>
     </apply>
    </apply>
   </bind>
  </apply>
 </apply>
</math>

Prefix

implies (eq ( S, ring ( R, add, zero, minus, mult, unit) , forall [ x y z ] . (implies (and (in ( x, R) , in ( y, R) , in ( z, R) ) , and (eq ( mult ( x, add ( y, z) ) , add ( mult ( x, y) , mult ( x, z) ) ) , eq ( mult ( add ( y, z) , x) , add ( mult ( y, x) , mult ( z, x) ) ) ) ) ) ) )

Popcorn

$S = ring1.ring($R, $add, $zero, $minus, $mult, $unit) = quant1.forall[$x, $y, $z -> set1.in($x, $R) and set1.in($y, $R) and set1.in($z, $R) ==> $mult($x, $add($y, $z)) = $add($mult($x, $y), $mult($x, $z)) and $mult($add($y, $z), $x) = $add($mult($y, $x), $mult($z, $x))]

Rendered Presentation MathML

$$S=\mathrm{ring}(R,\mathrm{add},\mathrm{zero},\mathrm{minus},\mathrm{mult},\mathrm{unit})=\forall \hspace{0.17em}x,y,z.x\in R\wedge y\in R\wedge z\in R\Rightarrow \mathrm{mult}(x,\mathrm{add}(y,z))=\mathrm{add}(\mathrm{mult}(x,y),\mathrm{mult}(x,z))\wedge \mathrm{mult}(\mathrm{add}(y,z),x)=\mathrm{add}(\mathrm{mult}(y,x),\mathrm{mult}(z,x))\Rightarrow$$

Example:

This example represents the ring which has as elements all rational integers. The ring addition is binary addition, the ring multiplication is binary multiplication.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="ring1" name="ring"/>
     <OMA><OMS cd="setname1" name="Z"/>
          <OMS cd="arith1" name="plus"/>
          <OMI>0</OMI>
          <OMS cd="arith1" name="minus"/>
          <OMS cd="arith1" name="times"/>
          <OMI>1</OMI>
     </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="ring1">ring</csymbol>
  <apply><csymbol cd="setname1">Z</csymbol>
   <csymbol cd="arith1">plus</csymbol>
   <cn>0</cn>
   <csymbol cd="arith1">minus</csymbol>
   <csymbol cd="arith1">times</csymbol>
   <cn>1</cn>
  </apply>
 </apply>
</math>

Prefix

ring (Z (plus, 0, minus, times, 1) )

Popcorn

ring1.ring(setname1.Z(arith1.plus, 0, arith1.minus, arith1.times, 1))

Rendered Presentation MathML

$$\mathrm{ring}\left(\mathbb{Z}\right)$$

Signatures:

sts

carrier

Description:

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

Example:

The carrier of ring(R,+,0,-,*,1) is R.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="ring1" name="carrier"/>
            <OMA><OMS cd="ring1" name="ring"/>
                 <OMV name="R"/>
                 <OMV name="plus"/>
                 <OMV name="zero"/>
                 <OMV name="minus"/>
                 <OMV name="times"/>
                 <OMV name="one"/>
            </OMA>
       </OMA>
       <OMV name="R"/>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="ring1">carrier</csymbol>
   <apply><csymbol cd="ring1">ring</csymbol>
    <ci>R</ci>
    <ci>plus</ci>
    <ci>zero</ci>
    <ci>minus</ci>
    <ci>times</ci>
    <ci>one</ci>
   </apply>
  </apply>
  <ci>R</ci>
 </apply>
</math>

Prefix

eq (carrier (ring ( R, plus, zero, minus, times, one) ) , R)

Popcorn

ring1.carrier(ring1.ring($R, $plus, $zero, $minus, $times, $one)) = $R

Rendered Presentation MathML

$$\mathrm{carrier}\left(\mathrm{ring}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one})\right)=R$$

Signatures:

sts

multiplication

Description:

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

Example:

The multiplication of ring(R,+,0,-,*,1) is *.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="ring1" name="multiplication"/>
            <OMA><OMS cd="ring1" name="ring"/>
                 <OMV name="R"/>
                 <OMV name="plus"/>
                 <OMV name="zero"/>
                 <OMV name="minus"/>
                 <OMV name="times"/>
                 <OMV name="one"/>
            </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="ring1">multiplication</csymbol>
   <apply><csymbol cd="ring1">ring</csymbol>
    <ci>R</ci>
    <ci>plus</ci>
    <ci>zero</ci>
    <ci>minus</ci>
    <ci>times</ci>
    <ci>one</ci>
   </apply>
  </apply>
  <ci>times</ci>
 </apply>
</math>

Prefix

eq (multiplication (ring ( R, plus, zero, minus, times, one) ) , times)

Popcorn

ring1.multiplication(ring1.ring($R, $plus, $zero, $minus, $times, $one)) = $times

Rendered Presentation MathML

$$\mathrm{multiplication}\left(\mathrm{ring}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one})\right)=\mathrm{times}$$

Signatures:

sts

negation

Description:

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

Example:

The minus of ring(R,+,0,-,*,1) is -.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="ring1" name="negation"/>
            <OMA><OMS cd="ring1" name="ring"/>
                 <OMV name="R"/>
                 <OMV name="plus"/>
                 <OMV name="zero"/>
                 <OMV name="minus"/>
                 <OMV name="times"/>
                 <OMV name="one"/>
            </OMA>
       </OMA>
       <OMV name="minus"/>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="ring1">negation</csymbol>
   <apply><csymbol cd="ring1">ring</csymbol>
    <ci>R</ci>
    <ci>plus</ci>
    <ci>zero</ci>
    <ci>minus</ci>
    <ci>times</ci>
    <ci>one</ci>
   </apply>
  </apply>
  <ci>minus</ci>
 </apply>
</math>

Prefix

eq (negation (ring ( R, plus, zero, minus, times, one) ) , minus)

Popcorn

ring1.negation(ring1.ring($R, $plus, $zero, $minus, $times, $one)) = $minus

Rendered Presentation MathML

$$\mathrm{negation}\left(\mathrm{ring}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one})\right)=\mathrm{minus}$$

Signatures:

sts

identity

Description:

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

Example:

The identity ring(R,+,0,-,*,1) is 1.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="ring1" name="identity"/>
            <OMA><OMS cd="ring1" name="ring"/>
                 <OMV name="R"/>
                 <OMV name="plus"/>
                 <OMV name="zero"/>
                 <OMV name="minus"/>
                 <OMV name="times"/>
                 <OMV name="one"/>
            </OMA>
       </OMA>
       <OMV name="one"/>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="ring1">identity</csymbol>
   <apply><csymbol cd="ring1">ring</csymbol>
    <ci>R</ci>
    <ci>plus</ci>
    <ci>zero</ci>
    <ci>minus</ci>
    <ci>times</ci>
    <ci>one</ci>
   </apply>
  </apply>
  <ci>one</ci>
 </apply>
</math>

Prefix

eq (identity (ring ( R, plus, zero, minus, times, one) ) , one)

Popcorn

ring1.identity(ring1.ring($R, $plus, $zero, $minus, $times, $one)) = $one

Rendered Presentation MathML

$$\mathrm{identity}\left(\mathrm{ring}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one})\right)=\mathrm{one}$$

Signatures:

sts

zero

Description:

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

Example:

The identity ring(R,+,0,-,*,1) is 0.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="ring1" name="zero"/>
            <OMA><OMS cd="ring1" name="ring"/>
                 <OMV name="R"/>
                 <OMV name="plus"/>
                 <OMV name="zero"/>
                 <OMV name="minus"/>
                 <OMV name="times"/>
                 <OMV name="one"/>
            </OMA>
       </OMA>
       <OMV name="zero"/>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="ring1">zero</csymbol>
   <apply><csymbol cd="ring1">ring</csymbol>
    <ci>R</ci>
    <ci>plus</ci>
    <ci>zero</ci>
    <ci>minus</ci>
    <ci>times</ci>
    <ci>one</ci>
   </apply>
  </apply>
  <ci>zero</ci>
 </apply>
</math>

Prefix

eq (zero (ring ( R, plus, zero, minus, times, one) ) , zero)

Popcorn

ring1.zero(ring1.ring($R, $plus, $zero, $minus, $times, $one)) = $zero

Rendered Presentation MathML

$$\mathrm{zero}\left(\mathrm{ring}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one})\right)=\mathrm{zero}$$

Signatures:

sts

addition

Description:

This symbols represents a unary function, whose argument should be a ring. It returns the addition on the ring. We will allow for the map to be n-ary.

Example:

The identity ring(R,+,0,-,*,1) is +.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="ring1" name="identity"/>
            <OMA><OMS cd="ring1" name="ring"/>
                 <OMV name="R"/>
                 <OMV name="plus"/>
                 <OMV name="zero"/>
                 <OMV name="minus"/>
                 <OMV name="times"/>
                 <OMV name="one"/>
            </OMA>
       </OMA>
       <OMV name="plus"/>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="ring1">identity</csymbol>
   <apply><csymbol cd="ring1">ring</csymbol>
    <ci>R</ci>
    <ci>plus</ci>
    <ci>zero</ci>
    <ci>minus</ci>
    <ci>times</ci>
    <ci>one</ci>
   </apply>
  </apply>
  <ci>plus</ci>
 </apply>
</math>

Prefix

eq (identity (ring ( R, plus, zero, minus, times, one) ) , plus)

Popcorn

ring1.identity(ring1.ring($R, $plus, $zero, $minus, $times, $one)) = $plus

Rendered Presentation MathML

$$\mathrm{identity}\left(\mathrm{ring}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one})\right)=\mathrm{plus}$$

Signatures:

sts

subtraction

Description:

This symbols represents a unary function, whose argument should be a ring. It returns the binary operation of subtraction on the ring.

Example:

The subtraction of ring(R,+,0,-,*,1) is the map sending the pair (r,s) of elements of R to r-s.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="ring1" name="subtraction"/>
            <OMA><OMS cd="ring1" name="ring"/>
                 <OMV name="R"/>
                 <OMV name="plus"/>
                 <OMV name="zero"/>
                 <OMV name="minus"/>
                 <OMV name="times"/>
                 <OMV name="one"/>
            </OMA>
       </OMA>
       <OMBIND><OMS cd="fns1" name="lambda"/>
            <OMBVAR><OMV name="x"/><OMV name="y"/>
            </OMBVAR>
            <OMA><OMV name="plus"/>
                 <OMV name="x"/>
                 <OMA><OMV name="minus"/>
                      <OMV name="y"/>
                 </OMA>
            </OMA>
       </OMBIND>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="ring1">subtraction</csymbol>
   <apply><csymbol cd="ring1">ring</csymbol>
    <ci>R</ci>
    <ci>plus</ci>
    <ci>zero</ci>
    <ci>minus</ci>
    <ci>times</ci>
    <ci>one</ci>
   </apply>
  </apply>
  <bind><csymbol cd="fns1">lambda</csymbol>
   <bvar><ci>x</ci></bvar>
   <bvar><ci>y</ci></bvar>
   <apply><ci>plus</ci><ci>x</ci><apply><ci>minus</ci><ci>y</ci></apply></apply>
  </bind>
 </apply>
</math>

Prefix

eq (subtraction (ring ( R, plus, zero, minus, times, one) ) , lambda [ x y ] . ( plus ( x, minus ( y) ) ) )

Popcorn

ring1.subtraction(ring1.ring($R, $plus, $zero, $minus, $times, $one)) = fns1.lambda[$x, $y -> $plus($x, $minus($y))]

Rendered Presentation MathML

$$\mathrm{subtraction}\left(\mathrm{ring}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one})\right)=\lambda \hspace{0.17em}x,y.\mathrm{plus}(x,\mathrm{minus}\left(y\right))$$

Signatures:

sts

is_commutative

Description:

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

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="ring1" 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="ring1" name="carrier"/>
              <OMV name="G"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMV name="b"/>
            <OMA>
              <OMS cd="ring1" name="carrier"/>
              <OMV name="G"/>
            </OMA>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
            <OMA>
              <OMS cd="ring1" name="multiplication"/>
              <OMV name="G"/>
            </OMA>
            <OMV name="a"/>
            <OMV name="b"/>
          </OMA>
          <OMA>
            <OMA>
              <OMS cd="ring1" 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="ring1">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="ring1">carrier</csymbol><ci>G</ci></apply>
     </apply>
     <apply><csymbol cd="set1">in</csymbol>
      <ci>b</ci>
      <apply><csymbol cd="ring1">carrier</csymbol><ci>G</ci></apply>
     </apply>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply><csymbol cd="ring1">multiplication</csymbol><ci>G</ci></apply>
     <ci>a</ci>
     <ci>b</ci>
    </apply>
    <apply>
     <apply><csymbol cd="ring1">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

ring1.is_commutative($G) ==> quant1.forall[$a, $b -> set1.in($a, ring1.carrier($G)) and set1.in($b, ring1.carrier($G)) ==> ring1.multiplication($G) = $a = $b ==> ring1.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

is_subring

Description:

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

Commented Mathematical property (CMP):

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

Signatures:

sts

additive_group

Description:

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

Example:

OpenMath XML (source)

    <OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
     <OMA><OMS cd="relation1" name="eq"/>
          <OMA><OMS cd="ring1" name="additive_group"/>
               <OMA><OMS cd="ring1" name="ring"/>
                    <OMV name="R"/> 
                    <OMV name="plus"/>
                    <OMV name="zero"/>
                    <OMV name="minus"/>
                    <OMV name="times"/>
                    <OMV name="one"/>
               </OMA>
          </OMA>
          <OMA><OMS cd="group1" name="group"/>
               <OMV name="R"/> 
               <OMV name="plus"/>
               <OMV name="zero"/>
               <OMV name="minus"/>
          </OMA>
     </OMA>
    </OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="ring1">additive_group</csymbol>
   <apply><csymbol cd="ring1">ring</csymbol>
    <ci>R</ci>
    <ci>plus</ci>
    <ci>zero</ci>
    <ci>minus</ci>
    <ci>times</ci>
    <ci>one</ci>
   </apply>
  </apply>
  <apply><csymbol cd="group1">group</csymbol>
   <ci>R</ci>
   <ci>plus</ci>
   <ci>zero</ci>
   <ci>minus</ci>
  </apply>
 </apply>
</math>

Prefix

eq (additive_group (ring ( R, plus, zero, minus, times, one) ) , group ( R, plus, zero, minus) )

Popcorn

ring1.additive_group(ring1.ring($R, $plus, $zero, $minus, $times, $one)) = group1.group($R, $plus, $zero, $minus)

Rendered Presentation MathML

$$\mathrm{additive\_group}\left(\mathrm{ring}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one})\right)=\mathrm{group}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus})$$

Signatures:

sts

multiplicative_monoid

Description:

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

Example:

OpenMath XML (source)

    <OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
     <OMA><OMS cd="relation1" name="eq"/>
          <OMA><OMS cd="ring1" name="multiplicative_monoid"/>
               <OMA><OMS cd="ring1" name="ring"/>
                    <OMV name="R"/> 
                    <OMV name="plus"/>
                    <OMV name="zero"/>
                    <OMV name="minus"/>
                    <OMV name="times"/>
                    <OMV name="one"/>
               </OMA>
          </OMA>
          <OMA><OMS cd="group1" name="monoid"/>
               <OMV name="R"/> 
               <OMV name="times"/>
               <OMV name="one"/>
          </OMA>
     </OMA>
    </OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="ring1">multiplicative_monoid</csymbol>
   <apply><csymbol cd="ring1">ring</csymbol>
    <ci>R</ci>
    <ci>plus</ci>
    <ci>zero</ci>
    <ci>minus</ci>
    <ci>times</ci>
    <ci>one</ci>
   </apply>
  </apply>
  <apply><csymbol cd="group1">monoid</csymbol><ci>R</ci><ci>times</ci><ci>one</ci></apply>
 </apply>
</math>

Prefix

eq (multiplicative_monoid (ring ( R, plus, zero, minus, times, one) ) , monoid ( R, times, one) )

Popcorn

ring1.multiplicative_monoid(ring1.ring($R, $plus, $zero, $minus, $times, $one)) = group1.monoid($R, $times, $one)

Rendered Presentation MathML

$$\mathrm{multiplicative\_monoid}\left(\mathrm{ring}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one})\right)=\mathrm{monoid}(R,\mathrm{times},\mathrm{one})$$

Signatures:

sts

expression

Description:

This symbol is a function with two arguments. Its first argument should be a ring. The second should be an arithmetic expression A, whose operators are times, plus, minus, unary_minus, and power, and whose leaves are members of the carrier of G. (Here an integer m will be interpreted as a member of G by interpreting it as the sum of m copies of the identity element, the symbol alg1.one will be interpreted as the identity, and the symbol alg1.zero will be interpreted as the zero of G.) When applied to G and A, it denotes the element (of G) that is the element obtained from the leaves by applying the arithmetic operations of G instead of those from the CD arith1.

Example:

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="ring1">expression</csymbol>
   <apply><csymbol cd="ring1">ring</csymbol>
    <csymbol cd="setname1">Z</csymbol>
    <csymbol cd="arith1">plus</csymbol>
    <cn>0</cn>
    <csymbol cd="arith1">unary_minus</csymbol>
    <csymbol cd="arith1">times</csymbol>
    <cn>1</cn>
   </apply>
   <apply><csymbol cd="arith1">times</csymbol><cn>6</cn><cn>3</cn></apply>
  </apply>
  <cn>18</cn>
 </apply>
</math>

Prefix

eq (expression (ring (Z, plus, 0, unary_minus, times, 1) , times (6, 3) ) , 18)

Popcorn

ring1.expression(ring1.ring(setname1.Z, arith1.plus, 0, arith1.unary_minus, arith1.times, 1), 6 * 3) = 18

Rendered Presentation MathML

$$\mathrm{expression}(\mathrm{ring}(\mathbb{Z},+,0,-,\times ,1),6\times 3)=18$$

Signatures:

sts

subring

Description:

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

Example:

OpenMath XML (source)

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

Strict Content MathML

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

Prefix

subring ( D, G)

Popcorn

ring1.subring($D, $G)

Rendered Presentation MathML

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

Example:

This example represents the subring of the multiplicative ring 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="ring1" name="subring"/>
     <OMA>
       <OMS cd="list1" name="list"/>
         <OMS cd="nums1" name="pi"/>
         <OMS cd="nums1" name="e"/>
     </OMA>
     <OMA><OMS cd="ring1" name="ring"/>
          <OMS cd="setname1" name="R"/>
          <OMS cd="arith1" name="plus"/>
          <OMI>0</OMI>
          <OMS cd="arith1" name="unary_minus"/>
          <OMS cd="arith1" name="times"/>
          <OMI> 1 </OMI>
     </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="ring1">subring</csymbol>
  <apply><csymbol cd="list1">list</csymbol>
   <csymbol cd="nums1">pi</csymbol>
   <csymbol cd="nums1">e</csymbol>
  </apply>
  <apply><csymbol cd="ring1">ring</csymbol>
   <csymbol cd="setname1">R</csymbol>
   <csymbol cd="arith1">plus</csymbol>
   <cn>0</cn>
   <csymbol cd="arith1">unary_minus</csymbol>
   <csymbol cd="arith1">times</csymbol>
   <cn>1</cn>
  </apply>
 </apply>
</math>

Prefix

subring (list (pi, e) , ring (R, plus, 0, unary_minus, times, 1 ) )

Popcorn

ring1.subring([nums1.pi , nums1.e], ring1.ring(setname1.R, arith1.plus, 0, arith1.unary_minus, arith1.times, 1))

Rendered Presentation MathML

$$\mathrm{subring}((\pi ,e),\mathrm{ring}(\mathbb{R},+,0,-,\times ,1))$$

Signatures:

sts

power

Description:

This is a symbol with two or three arguments. Its first argument should be a an element g of a ring and the second argument should be an integer. The optional third argument is the ring G containing g. 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="ring1" name="power"/>
            <OMI>3</OMI>
            <OMI>2</OMI>
            <OMA><OMS cd="ring1" name="ring"/>
                <OMS cd="setname1" name="Z"/>
                <OMS cd="arith1" name="plus"/>
                <OMI>0</OMI>
                <OMS cd="arith1" name="unary_minus"/>
                <OMS cd="arith1" name="times"/>
                <OMI>1</OMI>
            </OMA>
        </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="ring1">power</csymbol>
   <cn>3</cn>
   <cn>2</cn>
   <apply><csymbol cd="ring1">ring</csymbol>
    <csymbol cd="setname1">Z</csymbol>
    <csymbol cd="arith1">plus</csymbol>
    <cn>0</cn>
    <csymbol cd="arith1">unary_minus</csymbol>
    <csymbol cd="arith1">times</csymbol>
    <cn>1</cn>
   </apply>
  </apply>
  <cn>6</cn>
 </apply>
</math>

Prefix

eq (power (3, 2, ring (Z, plus, 0, unary_minus, times, 1) ) , 6)

Popcorn

ring1.power(3, 2, ring1.ring(setname1.Z, arith1.plus, 0, arith1.unary_minus, arith1.times, 1)) = 6

Rendered Presentation MathML

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

Signatures:

sts