Yamaguchi Lean 4 Library
Source: ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze
ProCGroups/ReidemeisterSchreier/Discrete/Presentations/Tietze/Source

Source: ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze

1import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.RelatorQuotientMutualMapData
2import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorMap
3import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.Core
4import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.RelatorReplacement
5import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorAddition
6import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorDeletion
7import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.Script
9/-!
10# Tietze equivalences and verified scripts
12This aggregate separates semantic presentation equivalence from syntactic
13transformations. The core and generator/relator operation modules construct
14certificates; `Tietze.Script` records well-typed elementary move sequences and
15their trace and cost.
16-/