Source: ProCGroups.ReidemeisterSchreier

1import ProCGroups.ReidemeisterSchreier.Discrete

2import ProCGroups.ReidemeisterSchreier.FreeGroup

3import ProCGroups.ReidemeisterSchreier.Profinite

5/-!

6# Reidemeister--Schreier theory

8Discrete and profinite forms of the Reidemeister--Schreier theorem, together with free-group word

9rewriting, presentation equivalence certificates, verified Tietze scripts, Schreier cocycles, and

10open-subgroup rank formulas.

12This is the public aggregate. For a smaller dependency surface, import

13`ProCGroups.ReidemeisterSchreier.Discrete`,

14`ProCGroups.ReidemeisterSchreier.Profinite`, or a focused submodule.