All.lean
Nyll.ProCGroups.LocalWeight.All
0 declarations indexed from sourceView source ↗
Module documentation
Local weight
This aggregate module exposes generating families converging to the identity and the resulting cardinal invariants, subgroup chains, metrizability criteria, and quotient estimates.
Imports6
- Nyll.ProCGroups.LocalWeight.CardinalInvariantsAndLocalWeight
- Nyll.ProCGroups.LocalWeight.ClosedNormalDataAndTransfiniteSeries
- Nyll.ProCGroups.LocalWeight.GeneratingSetsConvergingToOne
- Nyll.ProCGroups.LocalWeight.LocalWeightTheorems
- Nyll.ProCGroups.LocalWeight.MetrizabilityAndQuotients
- Nyll.ProCGroups.LocalWeight.SubgroupChains
Imported by1
This module has no indexed declarations. Its imports and full source are available here.