OpenMath Content Dictionary: alg1

Canonical URL:
http://www.openmath.org/cd/alg1.ocd
CD File:
alg1.ocd
CD as XML Encoded OpenMath:
alg1.omcd
Defines:
one, zero
Date:
2001-03-12
Version:
2
Review Date:
2003-04-01
Status:
official
Uses CD:
arith1, logic1, quant1, relation1, set1, setname1

A CD of basic algebraic concepts

At present this CD only holds definitions of zero and one. They are deliberately defined here without specifying any particular structure (e.g. a group) to which they correspond.


zero

This symbol represents the additive identity element.

Commented Mathematical property (CMP):
for all a | a + 0 = a
Formal Mathematical property (FMP):
<OMOBJ>
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
       <OMV name="a"/>
    </OMBVAR>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="arith1" name="plus"/>
        <OMV name="a"/>
        <OMS cd="alg1" name="zero"/>
      </OMA>
      <OMV name="a"/>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ a ] . (eq (plus ( a, zero) , a) )

Commented Mathematical property (CMP):
for all a | 0 * a = 0
Formal Mathematical property (FMP):
<OMOBJ>
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
       <OMV name="a"/>
    </OMBVAR>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="arith1" name="times"/>
        <OMS cd="alg1" name="zero"/>
        <OMV name="a"/>
      </OMA>
      <OMS cd="alg1" name="zero"/>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ a ] . (eq (times (zero, a) , zero) )

Commented Mathematical property (CMP):
The zero of the integers is 0
Formal Mathematical property (FMP):
<OMOBJ>
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
       <OMV name="x"/>
    </OMBVAR>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMA>
        <OMS cd="logic1" name="and"/>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMV name="x"/>
          <OMS cd="setname1" name="Z"/>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMV name="x"/>
          <OMS cd="alg1" name="zero"/>
        </OMA>
      </OMA>
      <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMV name="x"/>
      <OMI>0</OMI>
      </OMA>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ x ] . (implies (and (in ( x, Z) , eq ( x, zero) ) , eq ( x, 0) ) )

Signatures:
sts


[Next: one] [Last: one] [Top]

one

This symbol represents the multiplicative identity element.

Commented Mathematical property (CMP):
for all a | 1 * a = a
Formal Mathematical property (FMP):
<OMOBJ>
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
       <OMV name="a"/>
    </OMBVAR>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="arith1" name="times"/>
        <OMS cd="alg1" name="one"/>
        <OMV name="a"/>
      </OMA>
      <OMV name="a"/>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ a ] . (eq (times (one, a) , a) )

Commented Mathematical property (CMP):
for all a | a * 1 = a
Formal Mathematical property (FMP):
<OMOBJ>
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
       <OMV name="a"/>
    </OMBVAR>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="arith1" name="times"/>
        <OMV name="a"/>
        <OMS cd="alg1" name="one"/>
      </OMA>
      <OMV name="a"/>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ a ] . (eq (times ( a, one) , a) )

Commented Mathematical property (CMP):
The one of the integers is 1
Formal Mathematical property (FMP):
<OMOBJ>
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
       <OMV name="x"/>
    </OMBVAR>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMA>
        <OMS cd="logic1" name="and"/>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMV name="x"/>
          <OMS cd="setname1" name="Z"/>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMV name="x"/>
          <OMS cd="alg1" name="one"/>
        </OMA>
      </OMA>
      <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMV name="x"/>
      <OMI>1</OMI>
      </OMA>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ x ] . (implies (and (in ( x, Z) , eq ( x, one) ) , eq ( x, 1) ) )

Signatures:
sts


[First: zero] [Previous: zero] [Top]