## Definition ## Let $R$ be an [[ordered integral domain]], and let $inj: \mathbb{Z}_{+} \to R$ be the injection of the positive [[integers]] $\mathbb{Z}_{+}$ into $R$. ### With strict order ### $R$ is an __Archimedean ordered integral domain__ if there is a family of dependent terms $$a:R, b:R \vdash \alpha(a, b): ((0 \lt a) \times (0 \lt b)) \to \Vert \sum_{n:\mathbb{Z}_{+}} a \lt inj(n) \cdot b \Vert$$ ### With positivity ### $R$ is an __Archimedean ordered integral domain__ if there is a family of dependent terms $$a:R, b:R \vdash \alpha(a, b): (\mathrm{isPositive}(a) \times \mathrm{isPositive}(b)) \to \Vert \sum_{n:\mathbb{Z}_{+}} a \lt inj(n) \cdot b \Vert$$ ## Examples ## * The [[integers]] are an Archimedean ordered integral domain. * The [[rational numbers]] are a Archimedean ordered integral domain. * Every [[Archimedean ordered field]] is a Archimedean ordered integral domain. ## See also ## * [[ordered integral domain]] * [[Archimedean ordered abelian group]] * [[Archimedean ordered field]]