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

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 file also supports multiplicative groups via `MulArchimedean`

.

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}`

then `H`

is
generated by `a`

.

Given a subgroup `H`

of a decidable linearly ordered mul-archimedean abelian group `G`

, if there
exists a minimal element `a`

of `H ∩ G_{>1}`

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 a nontrivial subgroup of a linear ordered commutative group is disjoint
with the interval `Set.Ioo 1 a`

for some `1 < a`

, then the set of elements greater than 1 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.

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

for some `1 < a`

, then this is a cyclic subgroup.

Every subgroup of `ℤ`

is cyclic.