CompletedGroupAlgebra/UniversalProperty.lean

1import CompletedGroupAlgebra.UniversalProperty.Basic

2import CompletedGroupAlgebra.UniversalProperty.FiniteQuotient

3import CompletedGroupAlgebra.UniversalProperty.OpenSubmoduleQuotient

4import CompletedGroupAlgebra.UniversalProperty.ProfiniteModule

6/-

7PUBLIC_PAGE_SNAPSHOT

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

9lean_source: lean4/CompletedGroupAlgebra/UniversalProperty.lean

10translation_root: data/translation

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

12placement: after imports, never before imports

13-/

14/-!

15# Universal property of completed group algebras

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

18-/