All.lean
Nyll.ProCGroups.FiniteStepSolvableQuotients.All
0 declarations indexed from sourceView source ↗
Module documentation
Pro C Groups / Finite Step Solvable Quotients
This module formalizes the general constructions for finite-step solvable quotients. It also supplies the general ab-faithfulness, ab-torsion-freeness and slimness criteria used by geometric and arithmetic libraries.
Imports7
- Nyll.ProCGroups.FiniteStepSolvableQuotients.AbFaithfulness
- Nyll.ProCGroups.FiniteStepSolvableQuotients.AbTorsionFree
- Nyll.ProCGroups.FiniteStepSolvableQuotients.Faithful
- Nyll.ProCGroups.FiniteStepSolvableQuotients.SlimnessAndTorsion
- Nyll.ProCGroups.FiniteStepSolvableQuotients.Abelianization
- Nyll.ProCGroups.FiniteStepSolvableQuotients.Commutators.All
- Nyll.ProCGroups.FiniteStepSolvableQuotients.ProsolvableCriterion
Imported by1
This module has no indexed declarations. Its imports and full source are available here.