Yamaguchi Lean 4 Library
Homepage
Source: ProCGroups.ReidemeisterSchreier.Profinite
ProCGroups
/
ReidemeisterSchreier
/
Profinite
/
Source
Source: ProCGroups.ReidemeisterSchreier.Profinite
1
import
ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups
2
3
/-!
4
# Profinite Reidemeister--Schreier theory
5
6
This aggregate exports open-subgroup right-coset cocycles, exact generation,
7
and the proved finite-rank basis theorems for free pro-\(C\) groups.
8
-/