ReidemeisterSchreier/Discrete/ReidemeisterSchreier.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

11import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.Rewriting

12import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.Data

13import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.Tau

14import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.CleanedSymbols

15import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.CleanedTau

16import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.CleanedRelators

17import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.Kernel

18import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.WordCertificates

19import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.Presentation

20import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.TargetPresentation.Core

21import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.TargetPresentation.NormalWords

24PUBLIC_PAGE_SNAPSHOT

25generated_at: 2026-05-27T09:47:29+09:00

26lean_source: lean4/ReidemeisterSchreier/Discrete/ReidemeisterSchreier.lean

27translation_root: data/translation

28purpose: identifies the local data snapshot used to build pages/

29placement: after imports, never before imports

31/-!

32# Discrete Reidemeister-Schreier API

34This module re-exports the RS-specific rewriting and finite-quotient

35presentation API. Generic relator equivalence, normal-closure calculations, and

36Tietze transformations live in `ReidemeisterSchreier.Discrete.Presentations`.