All.lean
Nyll.ProCGroups.ProC.OpenNormalSubgroups.All
0 declarations indexed from sourceView source ↗
Module documentation
Open normal subgroups of pro-\(C\) groups
This aggregate collects the finite quotient, separation, basis, countable-chain, filtered-family, closed-commutator, and inverse-limit APIs built from open normal subgroups.
Imports9
- Nyll.ProCGroups.ProC.OpenNormalSubgroups.Basic
- Nyll.ProCGroups.ProC.OpenNormalSubgroups.BasisAtOne
- Nyll.ProCGroups.ProC.OpenNormalSubgroups.ClosedAndCosets
- Nyll.ProCGroups.ProC.OpenNormalSubgroups.ClosedCommutator
- Nyll.ProCGroups.ProC.OpenNormalSubgroups.CountableChains
- Nyll.ProCGroups.ProC.OpenNormalSubgroups.FilteredFamilies
- Nyll.ProCGroups.ProC.OpenNormalSubgroups.LimitPresentation
- Nyll.ProCGroups.ProC.OpenNormalSubgroups.ProCGroup
- Nyll.ProCGroups.ProC.OpenNormalSubgroups.Separation
Imported by1
This module has no indexed declarations. Its imports and full source are available here.