ReidemeisterSchreier.Discrete.OpenSubgroups.Words.Basic
This module develops the rewriting and basis constructions behind the subgroup calculations. It tracks words and relations through the chosen transversal to obtain the required presentation or basis statements.
def freeGroupInitialSegments {X : Type u} [DecidableEq X] (t : FreeGroup X) :
Set (FreeGroup X) := by
exact
{u | ∃ n ≤ (FreeGroup.toWord t).length, u = FreeGroup.mk (List.take n (FreeGroup.toWord t))}Initial segments of a free-group word are the prefixes used in the Reidemeister--Schreier rewriting.