Source: ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology
1import ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit
2import ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteComparison
4/-!
5# Completed Group Algebra / Open Finite Quotient Topology
7This aggregate exports coefficient-and-group finite quotients, the associated kernel topology,
8the opaque two-parameter inverse limit, its dense canonical map, and the comparison with the
9all-finite completed group algebra.
10-/