CompletedGroupAlgebra/Basic/InClass.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

8/-

9PUBLIC_PAGE_SNAPSHOT

10generated_at: 2026-05-27T09:47:29+09:00

11lean_source: lean4/CompletedGroupAlgebra/Basic/InClass.lean

12translation_root: data/translation

13purpose: identifies the local data snapshot used to build pages/

14placement: after imports, never before imports

15-/

16/-!

17# Completed group algebras

19The 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.

20-/