All.lean
Nyll.ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.All
0 declarations indexed from sourceView source ↗
Module documentation
Completed Group Algebra / Functoriality Within a Class
This aggregate exports \(C\)-indexed functoriality from quotient-index comaps through completed ring and algebra maps, group-like elements, comparison results, and the resulting continuous unit representation.
Imports6
- Nyll.ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.ComapIndex
- Nyll.ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.Comparison
- Nyll.ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.GroupLike
- Nyll.ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.Maps
- Nyll.ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.StageMaps
- Nyll.ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.UnitRepresentation
Imported by1
This module has no indexed declarations. Its imports and full source are available here.