All.lean
Nyll.ProCGroups.FreeProC.All
0 declarations indexed from sourceView source ↗
Module documentation
Free pro-C groups
This aggregate module exposes the construction and universal property of free pro-C groups, finite-basis and finite-generation results, canonical source data, characterizations, and applications to abelian and solvable quotients.
Imports11
- Nyll.ProCGroups.FreeProC.Abelianization
- Nyll.ProCGroups.FreeProC.Basic
- Nyll.ProCGroups.FreeProC.CanonicalData
- Nyll.ProCGroups.FreeProC.Characterization.All
- Nyll.ProCGroups.FreeProC.Criteria.All
- Nyll.ProCGroups.FreeProC.FiniteBasis
- Nyll.ProCGroups.FreeProC.FiniteRankSourceData
- Nyll.ProCGroups.FreeProC.FinitelyGenerated
- Nyll.ProCGroups.FreeProC.SolvableQuotients
- Nyll.ProCGroups.FreeProC.Universe
- Nyll.ProCGroups.FreeProC.Construction
Imported by1
This module has no indexed declarations. Its imports and full source are available here.