Subgroups of the integers

Stream: Is there code for X?

[Heather Macbeth]

Does mathlib have the classification of subgroups of $\mathbb{Z}$?

example (H : add_subgroup ℤ) : ∃ (a : ℤ), H = add_subgroup.closure {a}

[Kevin Buzzard]

I guess this could be proved for all subgroups of a cyclic group. And for all add_subgroups of an add_cyclic group...

[Heather Macbeth]

It can be generalised in several different directions (in addition to the direction you mention), the version I and Patrick currently have is:

import algebra.archimedean
import group_theory.subgroup

variables {G : Type*} [decidable_linear_ordered_add_comm_group G] [archimedean G]

lemma subgroup_cyclic_of_min {H : add_subgroup G} {a : G}
  (ha : is_least {g : G | g ∈ H ∧ 0 < g} a) : H = add_subgroup.closure {a} :=

[Heather Macbeth]

and Patrick also pointed out to me that it follows from the fact that subgroups of $\mathbb{Z}$ are ideals, via
docs#euclidean_domain.to_principal_ideal_domain
docs#int.euclidean_domain

[Heather Macbeth]

But is it possible that none of these versions are currently in mathlib? :)

[Heather Macbeth]

Kevin Buzzard said:

I guess this could be proved for all subgroups of a cyclic group. And for all add_subgroups of an add_cyclic group...

For the benefit of future readers -- this is docs#subgroup.is_cyclic

[Kevin Buzzard]

Is this only for multiplicative groups?

[Heather Macbeth]

Is there no @[to_additive] for that lemma? Oh no!

[Heather Macbeth]

now PR'd as docs#int.subgroup_cyclic