All.lean
Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.All
0 declarations indexed from sourceView source ↗
Module documentation
Tietze equivalences and verified scripts
This aggregate separates semantic presentation equivalence from syntactic transformations. The core and generator/relator operation modules construct certificates; Tietze.Script records well-typed elementary move sequences and their trace and cost.
Imports7
- Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.Core
- Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorAddition
- Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorDeletion
- Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorMap
- Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.RelatorQuotientMutualMapData
- Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.RelatorReplacement
- Nyll.ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.Script
This module has no indexed declarations. Its imports and full source are available here.