Yamaguchi Lean 4 Library
ProCGroups.ReidemeisterSchreier.FreeGroup
ProCGroups/ReidemeisterSchreier/FreeGroup

ProCGroups.ReidemeisterSchreier.FreeGroup

2 sections | 2 files | 39 declarations

This module formalizes free-group tools used in Reidemeister--Schreier rewriting.

imports
Imported by

Automorphisms

1 file | 8 declarations | 5 Theorems | 3 Definitions
This module constructs the free-group automorphism that inverts every generator, transports free bases along it, and proves the resulting automorphism is involutive.

PrefixParent

1 file | 31 declarations | 25 Theorems | 4 Definitions | 1 Abbreviation | 1 Structure
This module develops the signed-letter view of reduced free-group words, including cancellation at the last letter and the prefix-parent operation used to build Schreier prefix ...