Source: ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups

1import ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.BasisFiniteRank

2import ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.BasisTheorems

3import ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.DenseFreeModel

4import ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.ExactRightSchreierGeneration

5import ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.FinitePermutationTargets

6import ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.MinimalPower

7import ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.RankBound

8import ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.RightQuotient

9import ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.SchreierTransversals

11/-!

12# Profinite open-subgroup Reidemeister--Schreier theory

14This aggregate exports the concrete right-quotient and Schreier-cocycle

15constructions, exact right-Schreier generation, finite permutation targets,

16rank bounds, and finite-rank basis theorems for open subgroups of

17free pro-\(C\) groups.

19Basis conclusions use `EpimorphicallyFreeProCGroupOnConvergingSetData` directly. There is no

20parallel RS-specific carrier/model wrapper layer.