All.lean
Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.All
0 declarations indexed from sourceView source ↗
Module documentation
Presentation tools for Reidemeister--Schreier rewriting
This aggregate exports equality modulo normal closures, quotient-kernel presentations, presentation automation, semantic Tietze equivalences, and verified elementary Tietze scripts.
Imports4
This module has no indexed declarations. Its imports and full source are available here.