All.lean
Nyll.ProCGroups.ReidemeisterSchreier.All
0 declarations indexed from sourceView source ↗
Module documentation
Reidemeister--Schreier theory
Discrete and profinite forms of the Reidemeister--Schreier theorem, together with free-group word rewriting, presentation equivalence certificates, verified Tietze scripts, Schreier cocycles, and open-subgroup rank formulas.
This is the public aggregate. For a smaller dependency surface, import ProCGroups.ReidemeisterSchreier.Discrete, ProCGroups.ReidemeisterSchreier.Profinite, or a focused submodule.
Imports7
- Nyll.ProCGroups.ReidemeisterSchreier.Discrete.All
- Nyll.ProCGroups.ReidemeisterSchreier.FreeGroup.All
- Nyll.ProCGroups.ReidemeisterSchreier.Groupoid
- Nyll.ProCGroups.ReidemeisterSchreier.Profinite.All
- Nyll.ProCGroups.ReidemeisterSchreier.Quiver
- Nyll.ProCGroups.ReidemeisterSchreier.RightQuotient
- Nyll.ProCGroups.ReidemeisterSchreier.Schreier
Imported by1
This module has no indexed declarations. Its imports and full source are available here.