PolycyclicFiniteGeneration.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Finite generation of the lattice comparison groups

A cyclic series supplies finite generators at every step. This removes a separate finite-generation premise when a published lattice theorem gives polycyclicity.

theorem OAI.PolycyclicRecognition.finitelyGenerated_of_isCyclic line 20
Source documentation
A generator of a cyclic group is a finite generating set.
```
theorem finitelyGenerated_of_isCyclic [IsCyclic G] : Group.FG G := by
…
```
theorem OAI.PolycyclicRecognition.finitelyGenerated_of_cyclicStep line 26
Source documentation
Finite generation passes along a concrete cyclic extension.
```
theorem finitelyGenerated_of_cyclicStep {H K : Subgroup G} (s : CyclicStep H K)
    (hH : Group.FG H) : Group.FG K := by
…
```
theorem OAI.PolycyclicRecognition.finitelyGenerated_of_cyclicSeries line 44
Source documentation
The top group of a cyclic series is finitely generated when its initial group is finitely generated.
```
theorem finitelyGenerated_of_cyclicSeries {H K : Subgroup G} {n : ℕ}
    (c : CyclicSeries H K n) (hH : Group.FG H) : Group.FG K := by
…
```
theorem OAI.PolycyclicRecognition.IsPolycyclic.finitelyGenerated line 57
Source documentation
Every polycyclic group is finitely generated.
```
theorem IsPolycyclic.finitelyGenerated (hG : IsPolycyclic G) : Group.FG G := by
…
```
Mentions: OAI.PolycyclicRecognition.IsPolycyclic