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

theorem Rat.denseRange_cast {𝕜 : Type u_1} [] [] [] :
DenseRange Rat.cast

Rational numbers are dense in a linear ordered archimedean field.

theorem AddSubgroup.dense_of_not_isolated_zero {G : Type u_1} [] [] [] (S : ) (hS : ε > 0, gS, g Set.Ioo 0 ε) :
Dense S

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 ε.

theorem AddSubgroup.dense_of_no_min {G : Type u_1} [] [] [] (S : ) (hbot : S ) (H : ¬∃ (a : G), IsLeast {g : G | g S 0 < g} a) :
Dense S

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.

theorem AddSubgroup.dense_or_cyclic {G : Type u_1} [] [] [] (S : ) :
Dense S ∃ (a : G), S =

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.