NYLL
Module

All.lean

Nyll.ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.All
0 declarations indexed from sourceView source ↗

Module documentation

Profinite open-subgroup Reidemeister--Schreier theory

This aggregate exports the concrete right-quotient and Schreier-cocycle constructions, exact right-Schreier generation, finite permutation targets, rank bounds, and finite-rank basis theorems for open subgroups of free pro-\(C\) groups.

Basis conclusions use EpimorphicallyFreeProCGroupOnConvergingSetData directly. There is no parallel RS-specific carrier/model wrapper layer.

Imports9
Imported by1

Declarations

This module has no indexed declarations. Its imports and full source are available here.

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.