ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier

2 sections | 13 files | 370 declarations

This aggregate exposes the abstract rewriting construction together with its finite-quotient presentation pipeline.

imports
Imported by

FiniteQuotient

12 files | 234 declarations | 135 Theorems | 79 Definitions | 11 Abbreviations | 7 Structures | 2 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...

Rewriting

1 file | 136 declarations | 91 Theorems | 41 Definitions | 2 Abbreviations | 1 Structure | 1 Instance
This module defines abstract right Schreier representatives, their associated symbols and generators, and the rewriting maps that turn kernel words into words on Schreier symbols.