Yamaguchi Lean 4 Library
Source: ProCGroups.FiniteStepSolvableQuotients
ProCGroups/FiniteStepSolvableQuotients/Source

Source: ProCGroups.FiniteStepSolvableQuotients

1import ProCGroups.FiniteStepSolvableQuotients.AbelianActions
2import ProCGroups.FiniteStepSolvableQuotients.Abelianization
3import ProCGroups.FiniteStepSolvableQuotients.Commutators
5/-!
6# Pro C Groups / Finite Step Solvable Quotients
8This module formalizes finite-step solvable quotients and their abelian actions.
9-/