ReidemeisterSchreier/Discrete/OpenSubgroups/Words/Basic.lean
1import ReidemeisterSchreier.FreeGroup.PrefixParent
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ReidemeisterSchreier/Discrete/OpenSubgroups/Words/Basic.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Free-word compatibility for Schreier theory
14Free-group word lemmas, prefix-parent compatibility, Nielsen-Schreier calculations, and cancellation rules for Schreier generators.
15-/
17namespace ReidemeisterSchreier.Discrete.OpenSubgroups
20/-- The initial segments of the reduced word representing an element of a free group. -/
21def freeGroupInitialSegments {X : Type u} [DecidableEq X] (t : FreeGroup X) :
22 Set (FreeGroup X) := by
23 exact
24 {u | ∃ n ≤ (FreeGroup.toWord t).length, u = FreeGroup.mk (List.take n (FreeGroup.toWord t))}
27end ReidemeisterSchreier.Discrete.OpenSubgroups