Homotopy Type Theory Z-algebra > history (Rev #1)

Definition

A \mathbb{Z}-algebra is an abelian group (A,+,,0)(A, +, -, 0) with

  • a binary operation ()():A×AA(-)\cdot(-): A \times A \to A
  • a left distributive identity
    d λ: (a:G) (b:G) (c:G)a(b+c)=ab+acd_\lambda:\prod_{(a:G)} \prod_{(b:G)} \prod_{(c:G)} a \cdot (b + c) = a \cdot b + a \cdot c
  • a right distributive identity
    d ρ: (a:G) (b:G) (c:G)(a+b)c=ac+bcd_\rho:\prod_{(a:G)} \prod_{(b:G)} \prod_{(c:G)} (a + b) \cdot c = a \cdot c + b \cdot c

Examples

See also

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