# Topology on archimedean groups and fields #

In this file we prove the following theorems:

`Rat.denseRange_cast`

: the coercion from`ℚ`

to a linear ordered archimedean field has dense range;`AddSubgroup.dense_of_not_isolated_zero`

,`AddSubgroup.dense_of_no_min`

: two sufficient conditions for a subgroup of an archimedean linear ordered additive commutative group to be dense;`AddSubgroup.dense_or_cyclic`

: an additive subgroup of an archimedean linear ordered additive commutative group`G`

with order topology either is dense in`G`

or is a cyclic subgroup.

Rational numbers are dense in a linear ordered archimedean field.

An additive subgroup of an archimedean linear ordered additive commutative group with order
topology is dense provided that for all positive `ε`

there exists a positive element of the
subgroup that is less than `ε`

.

Let `S`

be a nontrivial additive subgroup in an archimedean linear ordered additive commutative
group `G`

with order topology. If the set of positive elements of `S`

does not have a minimal
element, then `S`

is dense `G`

.

An additive subgroup of an archimedean linear ordered additive commutative group `G`

with order
topology either is dense in `G`

or is a cyclic subgroup.