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 groupG
with order topology either is dense inG
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.