Homotopy Type Theory ordered integral domain > history (Rev #5, changes)

Showing changes from revision #4 to #5: Added | Removed | Changed

Definition

An ordered integral domain is a totally ordered commutative ring? which comes with a strict order $\lt$ such that

• $0 \lt 1$
• for all elements $a:R$ and $b:R$, if $0 \lt a$ and $0 \lt b$, then $0 \lt a + b$
• for all elements $a:R$ and $b:R$, if $0 \lt a$ and $0 \lt b$, then $0 \lt a \cdot b$
• for all elements $a:R$ and $b:R$, if $0 \lt \max(a, -a)$ and $0 \lt \max(b, -b)$, then $0 \lt \max(a \cdot b, -a \cdot b)$

Examples

• The integers are an ordered integral domain.

• The rational numbers are a ordered integral domain

• Every ordered field is a ordered integral domain.

See also

• ordered field

• unit interval

• Archimedean ordered integral domain