ProCGroups/FiniteStepSolvableQuotients.lean

1import ProCGroups.FiniteStepSolvableQuotients.AbelianActions.Faithful

2import ProCGroups.FiniteStepSolvableQuotients.AbelianActions.SlimnessAndTorsion

3import ProCGroups.FiniteStepSolvableQuotients.Abelianization

4import ProCGroups.FiniteStepSolvableQuotients.Commutators.Basic

5import ProCGroups.FiniteStepSolvableQuotients.Commutators.ClosureFromFiniteQuotients

6import ProCGroups.FiniteStepSolvableQuotients.Commutators.DerivedSeriesAndQuotients

7import ProCGroups.FiniteStepSolvableQuotients.Commutators.Width

9/-

10PUBLIC_PAGE_SNAPSHOT

11generated_at: 2026-05-27T09:47:29+09:00

12lean_source: lean4/ProCGroups/FiniteStepSolvableQuotients.lean

13translation_root: data/translation

14purpose: identifies the local data snapshot used to build pages/

15placement: after imports, never before imports

16-/

17/-!

18# Finite-step solvable quotients

20Develops topological derived series, maximal solvable quotients of bounded derived length, commutator closure formulas, and abelian-action consequences.

21-/