All.lean
Nyll.ProCGroups.ProC.InverseLimits.All
0 declarations indexed from sourceView source ↗
Module documentation
Inverse-limit constructions for pro-\(C\) groups
This aggregate exports finite pro-\(C\) quotient objects, inverse-limit models and quotient constructions, and standard predicates defined by the finite quotients in an open-normal basis.
Imports3
Imported by1
This module has no indexed declarations. Its imports and full source are available here.