Yamaguchi Lean 4 Library
ProCGroups.ReidemeisterSchreier.Profinite
ProCGroups/ReidemeisterSchreier/Profinite

ProCGroups.ReidemeisterSchreier.Profinite

1 section | 10 files | 121 declarations

This aggregate exports open-subgroup right-coset cocycles, exact generation, and the proved finite-rank basis theorems for free pro-\(C\) groups.

import
Imported by

OpenSubgroups

10 files | 121 declarations | 76 Theorems | 22 Definitions | 4 Abbreviations | 4 Structures | 1 Inductive | 14 Instances
Starting from a finite converging-set basis, this module constructs a basis of the open subgroup and proves the classical finite Schreier rank formula. The padding lemma works o...