Automation.lean
Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Automation
0 declarations indexed from sourceView source ↗
Module documentation
Reidemeister Schreier / Discrete / Presentations / Automation
This module defines the small proof automation used in relator calculations: it closes elementary RelatorEquivalent goals and reduces normal-closure membership goals to the standard closure lemmas.
Imports0
None.
This module has no indexed declarations. Its imports and full source are available here.