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

Definition

Given an ordered abelian group $A$ , let us inductively define the left action $act:\mathbb{N} \times A \to A$ as

act(0, a) \coloneqq a

act(s(n), a) \coloneqq act(n, a) + a

$A$ is an Archimedean ordered abelian group if there is a family of dependent terms

a:A, b:A \vdash \alpha(a, b): ((0 \lt a) \times (0 \lt b)) \to \Vert \sum_{n:\mathbb{N}} a \lt act(n, b) \Vert

Examples

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

See also

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