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

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

Definition

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

• a commutative identity for $\cdot$
  $$m_\kappa:\prod_{(a:G)} \prod_{(b:G)} 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

• Heyting integral field domain

• field?