Homotopy Type Theory discrete division Z-algebra > history (Rev #2, changes)

Definition

A discrete division $\mathbb{Z}$-algebra is a $\mathbb{Z}$-algebra $(A, +, -, 0, \cdot)$ with

• a discrete left divisibility identity
  $$d_\lambda:\prod_{(a:A)} ((a = 0) \to \emptyset) \times \prod_{(c:A)} \left\Vert \sum_{(b:A)} a \cdot b = c \right\Vert$$
• a discrete right divisibility identity
  $$d_\rho:\prod_{(a:A)} ((a = 0) \to \emptyset) \times \prod_{(c:A)} \left\Vert \sum_{(b:A)} b \cdot a = c \right\Vert$$

Examples

• The rational numbers are a discrete division $\mathbb{Z}$-algebra.

• Every discrete division ring is a discrete division $\mathbb{Z}$-algebra.

See also

• Z-algebra

• division Z-algebra