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

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

## 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$

### With strict order

$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$

### With positivity

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

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