All.lean
Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.All
0 declarations indexed from sourceView source ↗
Module documentation
Completed Group Algebra / All Finite Augmentation
This aggregate exports terminal-index and finite-stage augmentations, the canonical all-finite augmentation, its comparison with the \(C\)-indexed augmentation, and the completed augmentation ideal.
Imports5
- Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.AugmentationIdeal
- Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.CanonicalAugmentation
- Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.InClassComparison
- Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.StageAugmentation
- Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.TerminalIndex
Imported by1
This module has no indexed declarations. Its imports and full source are available here.