All.lean
Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.All
0 declarations indexed from sourceView source ↗
Module documentation
Relator toolkit
This aggregate module exposes the relator predicates, congruence constructions, free-group lifting lemmas, word operations, and presentation-level results used by the discrete Reidemeister--Schreier development.
Imports5
- Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Basic
- Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Congruence
- Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.FreeGroupLift
- Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Operations
- Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Presentation
This module has no indexed declarations. Its imports and full source are available here.