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

ProCGroups.ReidemeisterSchreier.Discrete

3 sections | 40 files | 755 declarations

This module formalizes the classical discrete Reidemeister--Schreier theorem.

imports
Imported by

OpenSubgroups

9 files | 78 declarations | 50 Theorems | 6 Lemmas | 18 Definitions | 2 Abbreviations | 2 Instances
This aggregate exposes the discrete open-subgroup development: reduced-word utilities, right Schreier transversals and generators, prefix trees, and the resulting free bases.

Presentations

17 files | 307 declarations | 159 Theorems | 139 Definitions | 4 Structures | 3 Inductive types | 2 Macros
This module defines the small proof automation used in relator calculations: it closes elementary `RelatorEquivalent` goals and reduces normal-closure membership goals to the st...

ReidemeisterSchreier

14 files | 370 declarations | 226 Theorems | 120 Definitions | 13 Abbreviations | 8 Structures | 3 Instances
This module removes relators attached to degenerate Schreier symbols, builds the finite cleaned relator set, and records the remaining quotient-section and augmented relator fam...