## 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 ## * [[abelian group]] * [[ordered integral domain]] * [[Archimedean ordered abelian group]]