ReidemeisterSchreier.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
31import ProCGroups.FreeConstructions.AmalgamsAndModules
32import ProCGroups.FreeConstructions.FiniteSubgroupBounds
33import ProCGroups.FreeProC.Characterization.EmbeddingProblems
34import ProCGroups.FreeProC.Characterization.FreenessAndLifting
35import ProCGroups.FreeProC.Characterization.InverseLimitTowers
36import ProCGroups.FreeProC.Characterization.Quasifree
37import ProCGroups.FreeProC.Constructions
38import ProCGroups.FreeProC.Criteria.AbstractResidual
39import ProCGroups.FreeProC.Criteria.InverseLimitsAndFiniteSubsets
40import ProCGroups.FreeProC.Spaces
41import ProCGroups.NormalSubgroups.MaximalIntersectionsAndSimpleRanks
42import ProCGroups.NormalSubgroups.PointedSumsAndSimpleQuotients
43import ProCGroups.NormalSubgroups.SimpleQuotients.Compactness
44import ProCGroups.Presentations.Profinite
45import ProCGroups.Presentations.SchreierTietze.Data
46import ProCGroups.Presentations.SchreierTietze.Relators
47import ProCGroups.Presentations.SchreierTietze.Restricted
48import ProCGroups.WreathProducts
49import ReidemeisterSchreier.Profinite.OpenSubgroups.Basic
50import ReidemeisterSchreier.Profinite.OpenSubgroups.BasisCardinalRank
51import ReidemeisterSchreier.Profinite.OpenSubgroups.BasisFiniteRank
52import ReidemeisterSchreier.Profinite.OpenSubgroups.BasisInfiniteRank
53import ReidemeisterSchreier.Profinite.OpenSubgroups.BasisTheorems
54import ReidemeisterSchreier.Profinite.OpenSubgroups.DenseFreeModel
55import ReidemeisterSchreier.Profinite.OpenSubgroups.ExactRightSchreierGeneration
56import ReidemeisterSchreier.Profinite.OpenSubgroups.FinitePermutationTargets
57import ReidemeisterSchreier.Profinite.OpenSubgroups.GeneratingFamilies
58import ReidemeisterSchreier.Profinite.OpenSubgroups.MinimalPower
59import ReidemeisterSchreier.Profinite.OpenSubgroups.RankBound
60import ReidemeisterSchreier.Profinite.OpenSubgroups.RightQuotient
61import ReidemeisterSchreier.Profinite.OpenSubgroups.SchreierTransversals
62import ReidemeisterSchreier.Profinite.SchreierFormula
64/-
65PUBLIC_PAGE_SNAPSHOT
66generated_at: 2026-05-27T09:47:29+09:00
67lean_source: lean4/ReidemeisterSchreier.lean
68translation_root: data/translation
69purpose: identifies the local data snapshot used to build pages/
70placement: after imports, never before imports
71-/
72/-!
73# Reidemeister-Schreier
75Public root for the discrete and profinite Reidemeister-Schreier APIs.
77For faster downstream builds, import `ReidemeisterSchreier.Discrete`,
78`ReidemeisterSchreier.Profinite`, or a focused submodule directly.
79-/