ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.Words
This aggregate exposes prefix operations on reduced free-group words and the compatibility layer connecting them to the Nielsen--Schreier action-groupoid construction.
imports
Basic
This module defines the initial reduced-word segments of a free-group element and proves the membership and prefix-parent facts used by discrete Schreier transversals.
NielsenSchreierCompat
This module connects the local word conventions with Mathlib's Nielsen--Schreier action-groupoid basis and establishes the edge and back-edge identities needed to transport that...