All.lean
Nyll.ProCGroups.FiniteGeneration.All
0 declarations indexed from sourceView source ↗
Module documentation
Topological finite generation
This aggregate module exposes the basic theory of topologically finitely generated groups, characteristic subgroup chains, and the associated finite-index bounds.
Imports3
Imported by1
This module has no indexed declarations. Its imports and full source are available here.