Yamaguchi Lean 4 Library
Source: ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation
ProCGroups/CompletedGroupAlgebra/ProfiniteModules/FiniteGroupAlgebra/Augmentation/Source

Source: ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation

1import ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Abstract
2import ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Completed
4/-!
5# Augmentation of finite and completed group algebras
7This aggregate exports algebraic augmentation and its ideal for group algebras together with the
8continuous augmentation obtained after completion.
9-/