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

• an identity showing that every term not equal to $0$ has a reciprocal (a two-sided multiplicative inverse)
  $$r:\prod_{(a:A)} \left( ((a = 0) \to \emptyset) \times \left\Vert \sum_{(b:A)} (a \cdot b = 1) \times (b \cdot a = 1) \right\Vert \right)$$

Examples

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

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

See also

• unital Z-algebra

• reciprocal Z-algebra