Solvable.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Solvable groups with finitely generated subgroups

Induction on the derived series proves that a solvable group whose subgroups are all finitely generated has a finite cyclic subnormal series. This is the algebraic step used for finitely generated nilpotent groups.

theorem OAI.PolycyclicRecognition.subgroups_fg_of_subgroups_fg line 21
Source documentation
Restricting to a subgroup preserves finite generation of all subgroups.
```
theorem subgroups_fg_of_subgroups_fg (hfg : ∀ J : Subgroup G, Group.FG J)
    (H : Subgroup G) : ∀ J : Subgroup H, Group.FG J := by
…
```
theorem OAI.PolycyclicRecognition.map_derivedSeries_commutator line 30
Source documentation
The derived series of the commutator subgroup maps to the shifted derived series of the ambient group.
```
theorem map_derivedSeries_commutator (n : ℕ) :
    (derivedSeries (commutator G) n).map (commutator G).subtype =
      derivedSeries G (n + 1) := by
…
```
theorem OAI.PolycyclicRecognition.isPolycyclic_of_derivedSeries_eq_bot line 43
Source documentation
A trivial term in the derived series and finite generation of every subgroup suffice to construct a finite cyclic series.
```
theorem isPolycyclic_of_derivedSeries_eq_bot (n : ℕ) :
    ∀ (G : Type*) [Group G], derivedSeries G n = ⊥ →
      (∀ J : Subgroup G, Group.FG J) → IsPolycyclic G := by
…
```
Mentions: OAI.PolycyclicRecognition.IsPolycyclic
theorem OAI.PolycyclicRecognition.isPolycyclic_of_solvable_subgroups_fg line 73
Source documentation
A solvable group with all subgroups finitely generated is polycyclic.
```
theorem isPolycyclic_of_solvable_subgroups_fg [Group.IsSolvable G]
    (hfg : ∀ J : Subgroup G, Group.FG J) : IsPolycyclic G := by
…
```
Mentions: OAI.PolycyclicRecognition.IsPolycyclic