Homotopy Type Theory discrete division ring > history (Rev #1)

Definition

A discrete division ring is a ring $(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$$

Properties

Every discrete division ring is a discrete reciprocal ring.

Examples

• The rational numbers are a discrete division ring.

• Every discrete reciprocal ring is a discrete division ring, and thus every discrete skewfield is a discrete division ring.

See also

• ring

• division ring