Yamaguchi Lean 4 Library
Homepage
Source: ProCGroups.ReidemeisterSchreier.FreeGroup
ProCGroups
/
ReidemeisterSchreier
/
FreeGroup
/
Source
Source: ProCGroups.ReidemeisterSchreier.FreeGroup
1
import
ProCGroups.ReidemeisterSchreier.FreeGroup.Automorphisms
2
import
ProCGroups.ReidemeisterSchreier.FreeGroup.PrefixParent
3
4
/-!
5
# Reidemeister Schreier / Free Group
6
7
This module formalizes free-group tools used in Reidemeister--Schreier rewriting.
8
-/