Yamaguchi Lean 4 Library
Source: ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators
ProCGroups/ReidemeisterSchreier/Discrete/Presentations/Relators/Source

Source: ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators

1import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Basic
2import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Congruence
3import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.FreeGroupLift
4import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Operations
5import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Presentation
7/-!
8# Relator toolkit
10This aggregate module exposes the relator predicates, congruence constructions,
11free-group lifting lemmas, word operations, and presentation-level results used
12by the discrete Reidemeister--Schreier development.
13-/