Source: ProCGroups.FiniteStepSolvableQuotients.Commutators
1import ProCGroups.FiniteStepSolvableQuotients.Commutators.Basic
2import ProCGroups.FiniteStepSolvableQuotients.Commutators.ClosureFromFiniteQuotients
3import ProCGroups.FiniteStepSolvableQuotients.Commutators.DerivedSeriesAndQuotients
4import ProCGroups.FiniteStepSolvableQuotients.Commutators.Width
6/-!
7# Closed commutators and their width
9This aggregate module exposes the closed derived series, its finite solvable quotients, closure
10criteria detected by finite quotients, and uniform commutator-width results.
11-/