ProCGroups.CompletedGroupAlgebra.Basic
This aggregate exports both opaque completed-group-algebra carriers, their finite-stage systems, bundled projections and topological structures, and the canonical comparison equivalence between the all-finite and \(C\)-indexed models.
imports
Imported by
AllFinite
This module defines the all-finite completed group algebra as a named inverse-limit carrier. Its compatible-family realization is available only through the explicit equivalence...
ClassComparison
This module compares the all-finite and \(C\)-indexed named completed carriers through their canonical projections, and bundles the resulting inverse maps as ring, algebra, and ...
InClass
This module defines the reverse-ordered open normal subgroups whose quotients lie in a finite-group class \(C\), together with their finite quotient groups and canonical quotien...