ReidemeisterSchreier/Discrete/Presentations/Tietze.lean
1import ReidemeisterSchreier.Discrete.Presentations.Tietze.RelatorQuotientMutualMapData
2import ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorMap
3import ReidemeisterSchreier.Discrete.Presentations.Tietze.Core
4import ReidemeisterSchreier.Discrete.Presentations.Tietze.RelatorReplacement
5import ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorAddition
6import ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorDeletion
7import ReidemeisterSchreier.Discrete.Presentations.Tietze.Script
9/-
10PUBLIC_PAGE_SNAPSHOT
11generated_at: 2026-05-27T09:47:29+09:00
12lean_source: lean4/ReidemeisterSchreier/Discrete/Presentations/Tietze.lean
13translation_root: data/translation
14purpose: identifies the local data snapshot used to build pages/
15placement: after imports, never before imports
16-/
17/-!
18# Tietze transformations for discrete presentations
20This module re-exports the generic presentation certificates:
21`RelatorQuotientMutualMapData`, `TietzeEquiv`, `Presentation`, and
22`TietzeScript`, together with relator replacement and generator
23addition/deletion constructors.
24-/