OpenMath Content Dictionary: ring4

Canonical URL:

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

CD Base:

http://www.openmath.org/cd

CD File:

ring4.ocd

CD as XML Encoded OpenMath:

ring4.omcd

Defines:

is_domain, is_field, is_maximal_ideal, is_prime_ideal, is_zero_divisor

Date:

2004-06-01

Version:

1 (Revision 1)

Review Date:

2006-06-01

Status:

experimental

---

A CD of functions for further basic properties of rings

Written by Arjeh M. Cohen 2004-02-25

---

is_maximal_ideal

Description:

The binary boolean function whose value is true iff the second argument is a maximal ideal of the first.

Signatures:

sts

---

[Next: is_prime_ideal] [Last: is_zero_divisor] [Top]

---

is_prime_ideal

Description:

The binary boolean function whose value is true iff the second argument is a prime ideal of the first.

Signatures:

sts

---

[Next: is_domain] [Previous: is_maximal_ideal] [Top]

---

is_domain

Description:

This symbol represents a boolean unary function. The argument is a ring R. When evaluated on R, the function returns true if R is a domain and false otherwise. A domain is a commutative ring without zero divisors.

Signatures:

sts

---

[Next: is_field] [Previous: is_prime_ideal] [Top]

---

is_field

Description:

This is unary boolean function whose argument should be a ring R. The value is true if and only if the ring is commutative and every nonzero element has a multiplicative inverse.

Commented Mathematical property (CMP):

If is_commutative(G) and for all a in carrier(G) there is b in carrier(G) such that a*b = identity(G), then is_field(G).

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="logic1" name="and"/>
            <OMA><OMS cd="ring1" name="is_commutative"/>
                 <OMV name="G"/>
            </OMA>
            <OMBIND><OMS cd="quant1" name="forall"/>
                 <OMBVAR> <OMV name="a"/> </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="relation1" name="neq"/>
                                <OMV name="a"/>
                                <OMA><OMS cd="ring1" name="zero"/>
                                     <OMV name="G"/>
                                </OMA>
                           </OMA>
                      </OMA>

                      <OMBIND><OMS cd="quant1" name="exists"/>
                           <OMBVAR> <OMV name="b"/> </OMBVAR>
                           <OMA><OMS cd="logic1" name="and"/>
                                <OMA><OMS cd="set1" name="in"/>
                                     <OMV name="b"/>
                                     <OMA><OMS cd="ring1" name="carrier"/>
                                          <OMV name="G"/>
                                     </OMA>
                                </OMA>
                                <OMA><OMS cd="relation1" name="eq"/>
                                     <OMA><OMA><OMS cd="ring1" name="multiplication"/>
                                               <OMV name="G"/>
                                          </OMA>
                                          <OMV name="a"/>
                                          <OMV name="b"/>
                                     </OMA>
                                     <OMA><OMS cd="ring1" name="identity"/>
                                          <OMV name="G"/>
                                     </OMA>
                                </OMA>
                           </OMA>
                      </OMBIND>
                 </OMA>
            </OMBIND>
       </OMA>
       <OMA><OMS cd="ring4" name="is_field"/>
            <OMV name="G"/>
       </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="logic1">and</csymbol>
   <apply><csymbol cd="ring1">is_commutative</csymbol><ci>G</ci></apply>
   <bind><csymbol cd="quant1">forall</csymbol>
    <bvar><ci>a</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="relation1">neq</csymbol>
       <ci>a</ci>
       <apply><csymbol cd="ring1">zero</csymbol><ci>G</ci></apply>
      </apply>
     </apply>
     <bind><csymbol cd="quant1">exists</csymbol>
      <bvar><ci>b</ci></bvar>
      <apply><csymbol cd="logic1">and</csymbol>
       <apply><csymbol cd="set1">in</csymbol>
        <ci>b</ci>
        <apply><csymbol cd="ring1">carrier</csymbol><ci>G</ci></apply>
       </apply>
       <apply><csymbol cd="relation1">eq</csymbol>
        <apply>
         <apply><csymbol cd="ring1">multiplication</csymbol><ci>G</ci></apply>
         <ci>a</ci>
         <ci>b</ci>
        </apply>
        <apply><csymbol cd="ring1">identity</csymbol><ci>G</ci></apply>
       </apply>
      </apply>
     </bind>
    </apply>
   </bind>
  </apply>
  <apply><csymbol cd="ring4">is_field</csymbol><ci>G</ci></apply>
 </apply>
</math>

Prefix

implies (and (is_commutative ( G) , forall [ a ] . (implies (and (in ( a, carrier ( G) ) , neq ( a, zero ( G) ) ) , exists [ b ] . (and (in ( b, carrier ( G) ) , eq (multiplication ( G) ( a, b) , identity ( G) ) ) ) ) ) ) , is_field ( G) )

Popcorn

ring1.is_commutative($G) and quant1.forall[$a -> set1.in($a, ring1.carrier($G)) and $a != ring1.zero($G) ==> quant1.exists[$b -> set1.in($b, ring1.carrier($G)) and ring1.multiplication($G)($a, $b) = ring1.identity($G)]] ==> ring4.is_field($G)

Rendered Presentation MathML

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

Signatures:

sts

---

[Next: is_zero_divisor] [Previous: is_domain] [Top]

---

is_zero_divisor

Description:

This symbol represents a boolean binary function. The first argument is a ring R, the second is an element x of R. When evaluated on R and x, the function returns true if x a zero divisor and nonzero in R.

Commented Mathematical property (CMP):

An element x of a ring R is a zero divisor if and only if it nonzero and there is a nonzero y in R such that x * y = 0 or y * x = 0.

Signatures:

sts

---

[First: is_maximal_ideal] [Previous: is_field] [Top]