Source: ProCGroups.ReidemeisterSchreier.Discrete
1import ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups
2import ProCGroups.ReidemeisterSchreier.Discrete.Presentations
3import ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier
4import ProCGroups.ReidemeisterSchreier.FreeGroup
5import ProCGroups.ReidemeisterSchreier.Schreier
7/-!
8# Reidemeister Schreier / Discrete
10This module formalizes the classical discrete Reidemeister--Schreier theorem.
11-/