Yamaguchi Lean 4 Library
Homepage
Source: ProCGroups.FreeConstructions
ProCGroups
/
FreeConstructions
/
Source
Source: ProCGroups.FreeConstructions
1
import
ProCGroups.FreeConstructions.FiniteSubgroupBounds
2
3
/-!
4
# Finite-subgroup generation bounds
5
6
The aggregate exports the concrete generating-data predicates and theorems
7
that concatenate finite generating families to bound the rank of the ambient
8
group.
9
-/