Source: ProCGroups.ReidemeisterSchreier.Discrete.Presentations
1import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Automation
2import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.KernelQuotient
3import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators
4import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze
6/-!
7# Presentation tools for Reidemeister--Schreier rewriting
9This aggregate exports equality modulo normal closures, quotient-kernel
10presentations, presentation automation, semantic Tietze equivalences, and
11verified elementary Tietze scripts.
12-/