#
Homotopy Type Theory
Archimedean ordered integral domain > history (Rev #6, changes)

Showing changes from revision #5 to #6:
Added | ~~Removed~~ | ~~Chan~~ged

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

## See also

Revision on June 15, 2022 at 18:28:40 by
Anonymous?.
See the history of this page for a list of all contributions to it.