# Homotopy Type Theory Archimedean ordered field > history (Rev #7, changes)

Showing changes from revision #6 to #7: Added | Removed | Changed

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