Homotopy Type Theory ring > history (Rev #2)

Definition

A ring is an unital $\mathbb{Z}$-algebra (A,+,,0,,1)(A, +, -, 0, \cdot, 1) with

  • an associative identity for \cdot
    m α: (a:G) (b:G) (c:G)(ab)c=a(bc)m_\alpha:\prod_{(a:G)} \prod_{(b:G)} \prod_{(c:G)} (a\cdot b)\cdot c = a\cdot (b\cdot c)

Properties

A ring is an A3-space in abelian groups.

Examples

See also

Revision on February 28, 2022 at 19:04:29 by Anonymous?. See the history of this page for a list of all contributions to it.