## Stream: Is there code for X?

### Topic: Subgroups of the integers

#### Heather Macbeth (Sep 29 2020 at 15:59):

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

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


#### Kevin Buzzard (Sep 29 2020 at 18:41):

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 (Sep 29 2020 at 18:44):

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 (Sep 29 2020 at 18:46):

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 (Sep 29 2020 at 18:46):

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

#### Heather Macbeth (Sep 29 2020 at 19:14):

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 (Sep 29 2020 at 19:17):

Is this only for multiplicative groups?

#### Heather Macbeth (Sep 29 2020 at 19:19):

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

#### Heather Macbeth (Oct 02 2020 at 04:18):

now PR'd as docs#int.subgroup_cyclic

Last updated: May 07 2021 at 22:14 UTC