Yamaguchi Lean 4 Library
Homepage
Source: ProCGroups.Abelian
ProCGroups
/
Abelian
/
Source
Source: ProCGroups.Abelian
1
import
ProCGroups.Abelian.TopologicalAbelianizationFunctoriality
2
import
ProCGroups.Abelian.TopologicalAbelianizationLimits
3
4
/-!
5
# Abelian constructions
6
7
This aggregate module exposes topological abelianization, its functoriality, and its compatibility
8
with inverse limits.
9
-/