CompletedGroupAlgebra/ProfiniteModules/Basic.lean

1import CompletedGroupAlgebra.ProfiniteModules.Basic.OpenIdeals

3/-

4PUBLIC_PAGE_SNAPSHOT

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

6lean_source: lean4/CompletedGroupAlgebra/ProfiniteModules/Basic.lean

7translation_root: data/translation

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

9placement: after imports, never before imports

10-/

11/-!

12# Profinite module structure

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

15-/