ReidemeisterSchreier/Discrete/OpenSubgroups.lean
1import ReidemeisterSchreier.Discrete.OpenSubgroups.FreeBasis
2import ReidemeisterSchreier.Discrete.OpenSubgroups.Generators
3import ReidemeisterSchreier.Discrete.OpenSubgroups.PrefixTree
4import ReidemeisterSchreier.Discrete.OpenSubgroups.Transversals
5import ReidemeisterSchreier.Discrete.OpenSubgroups.Words.Basic
6import ReidemeisterSchreier.Discrete.OpenSubgroups.Words.NielsenSchreierCompat
8/-
9PUBLIC_PAGE_SNAPSHOT
10generated_at: 2026-05-27T09:47:29+09:00
11lean_source: lean4/ReidemeisterSchreier/Discrete/OpenSubgroups.lean
12translation_root: data/translation
13purpose: identifies the local data snapshot used to build pages/
14placement: after imports, never before imports
15-/
16/-!
17# Discrete Open-Subgroup API
19This module re-exports Schreier transversals, subgroup generators, prefix-tree
20support, Nielsen-Schreier bases, and compatibility lemmas for open subgroups of
21free groups.
22-/