Source: ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier
1import ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient
2import ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.Rewriting
4/-!
5# Reidemeister Schreier / Discrete / Reidemeister Schreier
7This aggregate exposes the abstract rewriting construction together with its
8finite-quotient presentation pipeline.
9-/