ReidemeisterSchreier/Discrete/Presentations.lean
1import ReidemeisterSchreier.Discrete.Presentations.Relators
2import ReidemeisterSchreier.Discrete.Presentations.Tietze.RelatorQuotientMutualMapData
3import ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorMap
4import ReidemeisterSchreier.Discrete.Presentations.Tietze.Core
5import ReidemeisterSchreier.Discrete.Presentations.Tietze.RelatorReplacement
6import ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorAddition
7import ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorDeletion
8import ReidemeisterSchreier.Discrete.Presentations.Tietze.Script
9import ReidemeisterSchreier.Discrete.Presentations.KernelQuotient
10import ReidemeisterSchreier.Discrete.Presentations.Automation
12/-
13PUBLIC_PAGE_SNAPSHOT
14generated_at: 2026-05-27T09:47:29+09:00
15lean_source: lean4/ReidemeisterSchreier/Discrete/Presentations.lean
16translation_root: data/translation
17purpose: identifies the local data snapshot used to build pages/
18placement: after imports, never before imports
19-/
20/-!
21# Discrete presentation API
23This module re-exports the mathlib-only API for relator equivalence,
24normal-closure calculations, presented-group quotients, and Tietze
25transformations.
26-/