All.lean
Nyll.ProCGroups.FreeConstructions.All
0 declarations indexed from sourceView source ↗
Module documentation
Finite-subgroup generation bounds
The aggregate exports the concrete generating-data predicates and theorems that concatenate finite generating families to bound the rank of the ambient group.
Imports2
Imported by1
This module has no indexed declarations. Its imports and full source are available here.