Source: ProCGroups.CompletedGroupAlgebra.Basic.AllFinite
1import ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Topology
3/-!
4# Completed Group Algebra / Basic / All Finite
6This is the public aggregate for the all-finite completion \(\widehat{R[G]}\). It exports:
8* finite-quotient indices, stages, and transition maps;
9* the opaque named carrier and its explicit compatible-family equivalence;
10* the generic inverse-limit ring, module, and coefficient-algebra structures;
11* canonical bundled finite-stage projections and their linear, algebra, and continuous forms; and
12* the inverse-limit topological-ring, compactness, Hausdorff, and disconnectedness results.
14Downstream code should use `completedGroupAlgebraProjection`, `completedGroupAlgebra_ext`, and
15`completedGroupAlgebraCompatibleFamilyEquiv`; the concrete compatible-family subtype is not a
16second public carrier.
17-/