All.lean
Nyll.ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.All
0 declarations indexed from sourceView source ↗
Module documentation
Completed Group Algebra / Open Finite Quotient Topology
This aggregate exports coefficient-and-group finite quotients, the associated kernel topology, the opaque two-parameter inverse limit, its dense canonical map, and the comparison with the all-finite completed group algebra.
Imports5
- Nyll.ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.CanonicalMaps
- Nyll.ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.FiniteQuotients
- Nyll.ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteComparison
- Nyll.ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.All
- Nyll.ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteQuotients
Imported by1
This module has no indexed declarations. Its imports and full source are available here.