CompletedGroupAlgebra/Basic.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
15/-
16PUBLIC_PAGE_SNAPSHOT
17generated_at: 2026-05-27T09:47:29+09:00
18lean_source: lean4/CompletedGroupAlgebra/Basic.lean
19translation_root: data/translation
20purpose: identifies the local data snapshot used to build pages/
21placement: after imports, never before imports
22-/
23/-!
24# Completed group algebras
26The completed group algebra is presented as an inverse limit of finite group algebras, together with canonical augmentation, augmentation ideal, finite-stage maps, functoriality, and profinite module universal properties.
27-/