Abelian.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finitely generated abelian groups are polycyclic

Adjoining one generator to a subgroup of an abelian group gives a cyclic quotient. Iterating this observation constructs an actual finite cyclic subnormal series.

theorem OAI.PolycyclicRecognition.cyclicStep_closure_insert line 21
Source documentation
The quotient obtained by adjoining one generator to an abelian subgroup is cyclic.
```
theorem cyclicStep_closure_insert (S : Set G) (a : G) :
    CyclicStep (Subgroup.closure S) (Subgroup.closure (insert a S)) := by
…
```
theorem OAI.PolycyclicRecognition.exists_cyclicSeries_closure_finset line 61
Source documentation
A finite generating set in an abelian group explicitly yields a finite cyclic series from the trivial subgroup to its closure.
```
theorem exists_cyclicSeries_closure_finset (S : Finset G) :
    ∃ n : ℕ, Nonempty (CyclicSeries (⊥ : Subgroup G) (Subgroup.closure (S : Set G)) n) := by
…
```
theorem OAI.PolycyclicRecognition.isPolycyclic_of_finitelyGenerated_commGroup line 78
Source documentation
Every finitely generated abelian group is polycyclic.
```
theorem isPolycyclic_of_finitelyGenerated_commGroup (G : Type*) [CommGroup G]
    [Group.FG G] : IsPolycyclic G := by
…
```
Mentions: OAI.PolycyclicRecognition.IsPolycyclic