All.lean
Nyll.ProCGroups.ProC.Quotients.All
0 declarations indexed from sourceView source ↗
Module documentation
Quotients and sections of pro-\(C\) groups
This aggregate exports quotient topology results, left-quotient projections, continuous sections for open and closed subgroups, neighborhood approximation, and inverse systems formed from descending closed subgroups.
Imports6
- Nyll.ProCGroups.ProC.Quotients.ClosedNormal
- Nyll.ProCGroups.ProC.Quotients.ClosedSubgroupNeighborhoods
- Nyll.ProCGroups.ProC.Quotients.DescendingClosedSubgroupQuotients
- Nyll.ProCGroups.ProC.Quotients.LeftQuotientMaps
- Nyll.ProCGroups.ProC.Quotients.LeftQuotientProjectionSections
- Nyll.ProCGroups.ProC.Quotients.OpenSubgroupSections
Imported by1
This module has no indexed declarations. Its imports and full source are available here.