## Definition ## Let $R$ be an [[ordered field]], 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 field__ 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 field__ 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 [[rational numbers]] are a Archimedean ordered integral domain. ## See also ## * [[Archimedean ordered abelian group]] * [[Archimedean ordered integral domain]] * [[ordered field]]