OpenMath Content Dictionary: linalg5

Canonical URL:

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

CD Base:

http://www.openmath.org/cd

CD File:

linalg5.ocd

CD as XML Encoded OpenMath:

linalg5.omcd

Defines:

identity

Date:

2004-05-11

Version:

3 (Revision 1)

Review Date:

2006-03-30

Status:

experimental

This CD contains symbols which represent a number of special types of matrix.

identity

Role:

application

Description:

This symbol denotes a unary function which is used to construct an (nxn) identity matrix where n is the single positive integral argument.

Commented Mathematical property (CMP):

for all M | identity(rowcount M) * M = M * identity(columncount M) = M

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0" cdbase="http://www.openmath.org/cd">
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
      <OMV name="M"/>
    </OMBVAR>
    <OMA>
      <OMS cd="logic1" name="and"/>
      <OMA>
        <OMS cd="relation1" name="eq"/>
        <OMA>
          <OMS cd="arith1" name="times"/>
	  <OMA>
	    <OMS cd="linalg5" name="identity"/>
	    <OMA>
	      <OMS cd="linalg4" name="rowcount"/>
	      <OMV name="M"/>
	    </OMA>
	  </OMA>
	  <OMV name="M"/>
        </OMA>
        <OMV name="M"/>
      </OMA>
      <OMA>
        <OMS cd="relation1" name="eq"/>
        <OMA>
          <OMS cd="arith1" name="times"/>
	  <OMV name="M"/>
	  <OMA>
	    <OMS cd="linalg5" name="identity"/>
	    <OMA>
	      <OMS cd="linalg4" name="columncount"/>
	      <OMV name="M"/>
	    </OMA>
	  </OMA>
        </OMA>
        <OMV name="M"/>
      </OMA>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ M ] . (and (eq (times (identity (rowcount ( M) ) , M) , M) , eq (times ( M, identity (columncount ( M) ) ) , M) ) )

$$\forall \hspace{0.17em}M.\mathrm{identity}\left(\mathrm{rowcount}\left(M\right)\right)M=M\wedge M\mathrm{identity}\left(\mathrm{columncount}\left(M\right)\right)=M$$

Example:

A representation of the 2x2 identity matrix [[1,0],[0,1]]

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0" cdbase="http://www.openmath.org/cd">
  <OMA>
    <OMS cd="linalg5" name="identity"/>
    <OMI> 2 </OMI>
  </OMA>
</OMOBJ>

identity ( 2 )

$$\left(\begin{array}{cc}1& 0\\ 0& 1\end{array}\right)$$

Signatures:

sts

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0" cdbase="http://www.openmath.org/cd">
<OMA><OMS cd="list1" name="list"/>

	<OMA>
	  <OMS cd="complex1" name="complex-cartesian"/>
	  <OMI> 1 </OMI><OMI> 1 </OMI>
        </OMA>
         <OMA>
	  <OMS cd="complex1" name="complex-cartesian"/>
	  <OMI> 0 </OMI><OMI> 1 </OMI>
        </OMA>
         <OMA>
	  <OMS cd="complex1" name="complex-cartesian"/>
	  <OMI> 0 </OMI><OMI> 0 </OMI>
        </OMA>
         <OMA>
	  <OMS cd="complex1" name="complex-cartesian"/>
	  <OMI> 1 </OMI><OMI> 0 </OMI>
        </OMA>
         <OMA>
	  <OMS cd="complex1" name="complex-cartesian"/>
	  <OMI> 3 </OMI><OMI> 2 </OMI>
        </OMA>
         <OMA>
	  <OMS cd="complex1" name="complex-cartesian"/>
	  <OMI> 4 </OMI><OMA><OMS name="plus" cd="arith1"/><OMV name="x"/><OMI> 1 </OMI></OMA>
        </OMA>


        </OMA>
</OMOBJ>

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0" cdbase="http://www.openmath.org/cd">
<OMA><OMS cd="list1" name="list"/>

	<OMA>
	  <OMS cd="complex1" name="complex-polar"/>
	  <OMI> 1 </OMI><OMI> 1 </OMI>
        </OMA>
         <OMA>
	  <OMS cd="complex1" name="complex-polar"/>
	  <OMI> 0 </OMI><OMI> 1 </OMI>
        </OMA>
         <OMA>
	  <OMS cd="complex1" name="complex-polar"/>
	  <OMI> 0 </OMI><OMI> 0 </OMI>
        </OMA>
         <OMA>
	  <OMS cd="complex1" name="complex-polar"/>
	  <OMI> 1 </OMI><OMI> 0 </OMI>
        </OMA>
         <OMA>
	  <OMS cd="complex1" name="complex-polar"/>
	  <OMI> 3 </OMI><OMI> 2 </OMI>
        </OMA>
         <OMA>
	  <OMS cd="complex1" name="complex-polar"/>
	  <OMI> 4 </OMI><OMA><OMS name="plus" cd="arith1"/><OMV name="x"/><OMI> 1 </OMI></OMA>
        </OMA>


        </OMA>
</OMOBJ>