Homotopy Type Theory discrete integral domain > history (Rev #1)

Definition

A discrete integral domain is a discrete domain $(A, +, -, 0, \cdot, 1, #)$ with a commutative identity for $\cdot$:

Examples

• The integers are a discrete integral domain.

• The rational numbers are a discrete integral domain

• Every discrete field is a discrete integral domain.

See also

• ring

• integral domain