# Archimedean groups #

This file proves a few facts about ordered groups which satisfy the `Archimedean`

property, that is:
`class Archimedean (α) [OrderedAddCommMonoid α] : Prop :=`

`(arch : ∀ (x : α) {y}, 0 < y → ∃ n : ℕ, x ≤ n • y)∀ (x : α) {y}, 0 < y → ∃ n : ℕ, x ≤ n • y)→ ∃ n : ℕ, x ≤ n • y)∃ n : ℕ, x ≤ n • y)≤ n • y)`

They are placed here in a separate file (rather than incorporated as a continuation of
`Algebra.Order.Archimedean`

) because they rely on some imports from `GroupTheory`

-- bundled
subgroups in particular.

The main result is `AddSubgroup.cyclic_of_min`

: a subgroup of a decidable archimedean abelian
group is cyclic, if its set of positive elements has a minimal element.

This result is used in this file to deduce `Int.subgroup_cyclic`

, proving that every subgroup of `ℤ`

is cyclic. (There are several other methods one could use to prove this fact, including more purely
algebraic methods, but none seem to exist in mathlib as of writing. The closest is
`Subgroup.is_cyclic`

, but that has not been transferred to `AddSubgroup`

.)

The result is also used in `Topology.Instances.Real`

as an ingredient in the classification of
subgroups of `ℝ`

.

Given a subgroup `H`

of a decidable linearly ordered archimedean abelian group `G`

, if there
exists a minimal element `a`

of `H ∩ G_{>0}∩ G_{>0}`

then `H`

is generated by `a`

.

If a nontrivial additive subgroup of a linear ordered additive commutative group is disjoint
with the interval `Set.Ioo 0 a`

for some positive `a`

, then the set of positive elements of this
group admits the least element.

If an additive subgroup of a linear ordered additive commutative group is disjoint with the
interval `Set.Ioo 0 a`

for some positive `a`

, then this is a cyclic subgroup.

Every subgroup of `ℤ`

is cyclic.