All.lean
Nyll.ProCGroups.Topologies.FullSubgroupTopology.All
0 declarations indexed from sourceView source ↗
Module documentation
Full subgroup topologies
This aggregate exports abstract quotient formations and varieties, the associated notions of open and closed subgroup, pro-\(C\) closure and residuality, and pullback stability.
Imports2
Imported by1
This module has no indexed declarations. Its imports and full source are available here.