Yamaguchi Lean 4 Library
Homepage
Source: ProCGroups.LocalWeight
ProCGroups
/
LocalWeight
/
Source
Source: ProCGroups.LocalWeight
1
import
ProCGroups.LocalWeight.GeneratingSetsConvergingToOne
2
3
/-!
4
# Local weight
5
6
This aggregate module exposes generating families converging to the identity and the resulting
7
cardinal invariants, subgroup chains, metrizability criteria, and quotient estimates.
8
-/