NYLL
Module

Basic.lean

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.Words.Basic
1 declaration indexed from sourceView source ↗

Module documentation

Reidemeister Schreier / Discrete / Open Subgroups / Words / 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.

Imports1
Imported by2

Declarations

def

freeGroupInitialSegments

L26 ↗
ReidemeisterSchreier.Discrete.OpenSubgroups.freeGroupInitialSegments
Documentation

This list consists of the initial segments (prefixes) of the reduced word representing a free-group element, as used in Reidemeister--Schreier rewriting.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
Lean source · statement
def freeGroupInitialSegments {X : Type u} [DecidableEq X] (t : FreeGroup X) :
    Set (FreeGroup X)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.