Yamaguchi Lean 4 Library
Homepage
Source: ProCGroups.CompletedGroupAlgebra.Augmentation
ProCGroups
/
CompletedGroupAlgebra
/
Augmentation
/
Source
Source: ProCGroups.CompletedGroupAlgebra.Augmentation
1
import
ProCGroups.CompletedGroupAlgebra.Augmentation.Functoriality
2
3
/-!
4
# Completed Group Algebra / Augmentation
5
6
This aggregate exports the \(C\)-indexed stage and canonical augmentations, the augmentation ideal,
7
and functoriality of these constructions.
8
-/