Source: ProCGroups.CompletedGroupAlgebra.InClassFunctoriality
1import ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.UnitRepresentation
3/-!
4# Completed Group Algebra / Functoriality Within a Class
6This aggregate exports \(C\)-indexed functoriality from quotient-index comaps through completed
7ring and algebra maps, group-like elements, comparison results, and the resulting continuous unit
8representation.
9-/