Homotopy Type Theory ordered abelian group > history (Rev #1)

Definition

An ordered abelian group is an abelian group $A$ with a strict order $\lt$ and a family of dependent terms

a:A, b:A \vdash \alpha(a, b): (0 \lt a) \times (0 \lt b) \to (0 \lt a + b)

Examples

The integers are an ordered abelian group
The rational numbers are an ordered abelian group
Every ordered integral domain is an ordered abelian group

See also

Revision on March 12, 2022 at 22:04:32 by Anonymous?. See the history of this page for a list of all contributions to it.