Homotopy Type Theory commutative ring > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Definition

A commutative ring is a ring $(A, +, -, 0, \cdot, 1)$ with

• a commutative identity for $\cdot$
  $$m_{\kappa }:\prod _{(a:\mathrm{<span><del\; class="diffmod">\; G</del><ins\; class="diffmod">\; A</ins></span>})}\prod _{(b:\mathrm{<span><del\; class="diffmod">\; G</del><ins\; class="diffmod">\; A</ins></span>})}a\cdot b=b\cdot a$$ m_\kappa:\prod_{(a:G)} m_\kappa:\prod_{(a:A)} \prod_{(b:G)} \prod_{(b:A)} a\cdot b = b\cdot a

Properties

A commutative ring is a commutative A3-space in abelian groups.

Examples

• Every contractible type is a commutative ring.

• The integers are a commutative ring.

• The rational numbers are a commutative ring.

See also

• commutative A3-space

• ring

• integral domain

• field?