CompletedGroupAlgebra.lean
1import CompletedGroupAlgebra.Basic.InClass.Index
2import CompletedGroupAlgebra.Basic.InClass.Stage
3import CompletedGroupAlgebra.Basic.InClass.System
4import CompletedGroupAlgebra.Basic.InClass.LimitAlgebra
5import CompletedGroupAlgebra.Basic.InClass.Projection
6import CompletedGroupAlgebra.Basic.InClass.Topology
7import CompletedGroupAlgebra.Basic.AllFinite.Index
8import CompletedGroupAlgebra.Basic.AllFinite.Stage
9import CompletedGroupAlgebra.Basic.AllFinite.Additive
10import CompletedGroupAlgebra.Basic.AllFinite.Ring
11import CompletedGroupAlgebra.Basic.AllFinite.Projections
12import CompletedGroupAlgebra.Basic.AllFinite.Topology
13import CompletedGroupAlgebra.Basic.ClassComparison
14import CompletedGroupAlgebra.OpenFiniteQuotientTopology.CanonicalMaps
15import CompletedGroupAlgebra.OpenFiniteQuotientTopology.FiniteQuotients
16import CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteQuotients
17import CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.CanonicalMap
18import CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteComparison
19import CompletedGroupAlgebra.AllFiniteFunctoriality.Comap
20import CompletedGroupAlgebra.AllFiniteFunctoriality.StageMap
21import CompletedGroupAlgebra.AllFiniteFunctoriality.Map
22import CompletedGroupAlgebra.AllFiniteFunctoriality.Surjectivity
23import CompletedGroupAlgebra.AllFiniteFunctoriality.InClassNaturality
24import CompletedGroupAlgebra.AllFiniteFunctoriality.GroupLike
25import CompletedGroupAlgebra.InClassFunctoriality.ComapIndex
26import CompletedGroupAlgebra.InClassFunctoriality.StageMaps
27import CompletedGroupAlgebra.InClassFunctoriality.Maps
28import CompletedGroupAlgebra.InClassFunctoriality.GroupLike
29import CompletedGroupAlgebra.InClassFunctoriality.Comparison
30import CompletedGroupAlgebra.InClassFunctoriality.UnitRepresentation
31import CompletedGroupAlgebra.Augmentation.StageAugmentation
32import CompletedGroupAlgebra.Augmentation.CanonicalAugmentation
33import CompletedGroupAlgebra.Augmentation.AugmentationIdeal
34import CompletedGroupAlgebra.Augmentation.Functoriality
35import CompletedGroupAlgebra.AllFiniteAugmentation.TerminalIndex
36import CompletedGroupAlgebra.AllFiniteAugmentation.StageAugmentation
37import CompletedGroupAlgebra.AllFiniteAugmentation.CanonicalAugmentation
38import CompletedGroupAlgebra.AllFiniteAugmentation.InClassComparison
39import CompletedGroupAlgebra.AllFiniteAugmentation.AugmentationIdeal
40import CompletedGroupAlgebra.UniversalProperty.Basic
41import CompletedGroupAlgebra.UniversalProperty.FiniteQuotient
42import CompletedGroupAlgebra.UniversalProperty.OpenSubmoduleQuotient
43import CompletedGroupAlgebra.UniversalProperty.ProfiniteModule
44import CompletedGroupAlgebra.FunctorialityComposition
45import CompletedGroupAlgebra.ProfiniteModules.Basic.OpenIdeals
46import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Topology
47import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Functoriality
48import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Abstract
49import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Completed
50import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.UnitRepresentation
52/-
53PUBLIC_PAGE_SNAPSHOT
54generated_at: 2026-05-27T09:47:29+09:00
55lean_source: lean4/CompletedGroupAlgebra.lean
56translation_root: data/translation
57purpose: identifies the local data snapshot used to build pages/
58placement: after imports, never before imports
59-/
60/-!
61# Completed group algebra
63Public entry point for completed group algebras, augmentation maps, augmentation ideals,
65-/