Homotopy Type Theory ring > history (Rev #7)

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)

Examples

See also

Revision on June 13, 2022 at 06:15:48 by Anonymous?. See the history of this page for a list of all contributions to it.