ReidemeisterSchreier/Profinite.lean
1import ProCGroups.FreeConstructions.AmalgamsAndModules
2import ProCGroups.FreeConstructions.FiniteSubgroupBounds
3import ProCGroups.FreeProC.Characterization.EmbeddingProblems
4import ProCGroups.FreeProC.Characterization.FreenessAndLifting
5import ProCGroups.FreeProC.Characterization.InverseLimitTowers
6import ProCGroups.FreeProC.Characterization.Quasifree
7import ProCGroups.FreeProC.Constructions
8import ProCGroups.FreeProC.Criteria.AbstractResidual
9import ProCGroups.FreeProC.Criteria.InverseLimitsAndFiniteSubsets
10import ProCGroups.FreeProC.Spaces
11import ProCGroups.NormalSubgroups.MaximalIntersectionsAndSimpleRanks
12import ProCGroups.NormalSubgroups.PointedSumsAndSimpleQuotients
13import ProCGroups.NormalSubgroups.SimpleQuotients.Compactness
14import ProCGroups.Presentations.Profinite
15import ProCGroups.Presentations.SchreierTietze.Data
16import ProCGroups.Presentations.SchreierTietze.Relators
17import ProCGroups.Presentations.SchreierTietze.Restricted
18import ProCGroups.WreathProducts
19import ReidemeisterSchreier.Profinite.OpenSubgroups.Basic
20import ReidemeisterSchreier.Profinite.OpenSubgroups.BasisCardinalRank
21import ReidemeisterSchreier.Profinite.OpenSubgroups.BasisFiniteRank
22import ReidemeisterSchreier.Profinite.OpenSubgroups.BasisInfiniteRank
23import ReidemeisterSchreier.Profinite.OpenSubgroups.BasisTheorems
24import ReidemeisterSchreier.Profinite.OpenSubgroups.DenseFreeModel
25import ReidemeisterSchreier.Profinite.OpenSubgroups.ExactRightSchreierGeneration
26import ReidemeisterSchreier.Profinite.OpenSubgroups.FinitePermutationTargets
27import ReidemeisterSchreier.Profinite.OpenSubgroups.GeneratingFamilies
28import ReidemeisterSchreier.Profinite.OpenSubgroups.MinimalPower
29import ReidemeisterSchreier.Profinite.OpenSubgroups.RankBound
30import ReidemeisterSchreier.Profinite.OpenSubgroups.RightQuotient
31import ReidemeisterSchreier.Profinite.OpenSubgroups.SchreierTransversals
32import ReidemeisterSchreier.Profinite.SchreierFormula
34/-
35PUBLIC_PAGE_SNAPSHOT
36generated_at: 2026-05-27T09:47:29+09:00
37lean_source: lean4/ReidemeisterSchreier/Profinite.lean
38translation_root: data/translation
39purpose: identifies the local data snapshot used to build pages/
40placement: after imports, never before imports
41-/
42/-!
43# Profinite Reidemeister-Schreier API
45This module collects the profinite/open-subgroup interface. It intentionally
46avoids importing the full discrete root module or application-specific FreeProC
47canonical data; profinite files import only the discrete submodules they need.
48-/