ReidemeisterSchreier/Profinite/OpenSubgroups.lean
1import ReidemeisterSchreier.Profinite.OpenSubgroups.Basic
2import ReidemeisterSchreier.Profinite.OpenSubgroups.BasisCardinalRank
3import ReidemeisterSchreier.Profinite.OpenSubgroups.BasisFiniteRank
4import ReidemeisterSchreier.Profinite.OpenSubgroups.BasisInfiniteRank
5import ReidemeisterSchreier.Profinite.OpenSubgroups.BasisTheorems
6import ReidemeisterSchreier.Profinite.OpenSubgroups.DenseFreeModel
7import ReidemeisterSchreier.Profinite.OpenSubgroups.ExactRightSchreierGeneration
8import ReidemeisterSchreier.Profinite.OpenSubgroups.FinitePermutationTargets
9import ReidemeisterSchreier.Profinite.OpenSubgroups.GeneratingFamilies
10import ReidemeisterSchreier.Profinite.OpenSubgroups.MinimalPower
11import ReidemeisterSchreier.Profinite.OpenSubgroups.RankBound
12import ReidemeisterSchreier.Profinite.OpenSubgroups.RightQuotient
13import ReidemeisterSchreier.Profinite.OpenSubgroups.SchreierTransversals
15/-
16PUBLIC_PAGE_SNAPSHOT
17generated_at: 2026-05-27T09:47:29+09:00
18lean_source: lean4/ReidemeisterSchreier/Profinite/OpenSubgroups.lean
19translation_root: data/translation
20purpose: identifies the local data snapshot used to build pages/
21placement: after imports, never before imports
22-/
23/-!
24# Profinite Open-Subgroup API
26This module re-exports the completed profinite open-subgroup results:
27Schreier transversals, dense free models, exact right-Schreier generation,
29-/