ProCGroups/Abelian.lean
1import ProCGroups.Abelian.TopologicalAbelianization
2import ProCGroups.Abelian.TopologicalAbelianizationFunctoriality
3import ProCGroups.Abelian.TopologicalAbelianizationLimits
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/Abelian.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Topological abelianization API
16This module re-exports the public topological abelianization construction,
18-/