## 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$$ ## 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 ## * [[ordered abelian group]] * [[Archimedean ordered integral domain]] category: not redirected to nlab yet