Yamaguchi Lean 4 Library
ReidemeisterSchreier.Discrete.ReidemeisterSchreier
ReidemeisterSchreier/Discrete/ReidemeisterSchreier

ReidemeisterSchreier.Discrete.ReidemeisterSchreier

2 sections | 13 files | 381 declarations

This module develops Reidemeister--Schreier rewriting, Schreier generators, finite quotient transversals, and presentation transformations.

FiniteQuotient

12 files | 245 declarations | 145 Theorem | 80 Definition | 11 Abbreviation | 7 Structure | 2 Instance
This is the relator family obtained by rewriting original relators and then deleting degenerate Schreier generators.

Rewriting

1 files | 136 declarations | 91 Theorem | 41 Definition | 2 Abbreviation | 1 Structure | 1 Instance
A normalized representative function for right cosets of \(L\) in a free group. The condition \(g(\operatorname{rep}(g))^{-1}\in L\) says that \(\operatorname{rep}(g)\) represen...