ReidemeisterSchreier/Discrete.lean

1import ReidemeisterSchreier.FreeGroup.Automorphisms

2import ReidemeisterSchreier.FreeGroup.PrefixParent

3import ReidemeisterSchreier.Discrete.Presentations.Relators

4import ReidemeisterSchreier.Discrete.Presentations.Tietze.RelatorQuotientMutualMapData

5import ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorMap

6import ReidemeisterSchreier.Discrete.Presentations.Tietze.Core

7import ReidemeisterSchreier.Discrete.Presentations.Tietze.RelatorReplacement

8import ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorAddition

9import ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorDeletion

10import ReidemeisterSchreier.Discrete.Presentations.Tietze.Script

11import ReidemeisterSchreier.Discrete.Presentations.KernelQuotient

12import ReidemeisterSchreier.Discrete.Presentations.Automation

13import ReidemeisterSchreier.Discrete.OpenSubgroups.FreeBasis

14import ReidemeisterSchreier.Discrete.OpenSubgroups.Generators

15import ReidemeisterSchreier.Discrete.OpenSubgroups.PrefixTree

16import ReidemeisterSchreier.Discrete.OpenSubgroups.Transversals

17import ReidemeisterSchreier.Discrete.OpenSubgroups.Words.Basic

18import ReidemeisterSchreier.Discrete.OpenSubgroups.Words.NielsenSchreierCompat

19import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.Rewriting

20import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.Data

21import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.Tau

22import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.CleanedSymbols

23import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.CleanedTau

24import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.CleanedRelators

25import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.Kernel

26import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.WordCertificates

27import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.Presentation

28import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.TargetPresentation.Core

29import ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.TargetPresentation.NormalWords

30import ReidemeisterSchreier.Schreier

33PUBLIC_PAGE_SNAPSHOT

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

35lean_source: lean4/ReidemeisterSchreier/Discrete.lean

36translation_root: data/translation

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

38placement: after imports, never before imports

40/-!

41# Discrete Reidemeister-Schreier Theory

43This module re-exports the mathlib-only discrete FreeGroup helpers,

44open-subgroup Schreier bases, generic presentation/Tietze API, finite

45Reidemeister-Schreier presentations, and relator automation.