CompletedGroupAlgebra/AllFiniteFunctoriality.lean

1import CompletedGroupAlgebra.AllFiniteFunctoriality.Comap
2import CompletedGroupAlgebra.AllFiniteFunctoriality.StageMap
3import CompletedGroupAlgebra.AllFiniteFunctoriality.Map
4import CompletedGroupAlgebra.AllFiniteFunctoriality.Surjectivity
5import CompletedGroupAlgebra.AllFiniteFunctoriality.InClassNaturality
6import CompletedGroupAlgebra.AllFiniteFunctoriality.GroupLike
8/-
9PUBLIC_PAGE_SNAPSHOT
10generated_at: 2026-05-27T09:47:29+09:00
11lean_source: lean4/CompletedGroupAlgebra/AllFiniteFunctoriality.lean
12translation_root: data/translation
13purpose: identifies the local data snapshot used to build pages/
14placement: after imports, never before imports
15-/
16/-!
17# All-finite completed group algebra functoriality
19Import aggregator for all-finite completed group algebra functoriality in the group variable.
20-/