All.lean
Nyll.ProCGroups.CompletedGroupAlgebra.Basic.All
0 declarations indexed from sourceView source ↗
Module documentation
Completed Group Algebra / 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.
Imports3
Imported by1
This module has no indexed declarations. Its imports and full source are available here.