Yamaguchi Lean 4 Library
ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.TargetPresentation
ProCGroups/ReidemeisterSchreier/Discrete/ReidemeisterSchreier/FiniteQuotient/TargetPresentation

ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.TargetPresentation

2 sections | 2 files | 42 declarations

This aggregate exposes the certificate data and normal-word construction which identify the cleaned finite-quotient presentation with the target kernel presentation.

imports
Imported by

Core

1 file | 35 declarations | 3 Theorems | 18 Definitions | 8 Abbreviations | 5 Structures | 1 Instance
Reidemeister Schreier / Discrete / Reidemeister Schreier / Finite Quotient / Target Presentation / Core. This module defines the structured certificates for prefix-closed quotie...

NormalWords

1 file | 7 declarations | 1 Theorem | 5 Definitions | 1 Structure
Reidemeister Schreier / Discrete / Reidemeister Schreier / Finite Quotient / Target Presentation / Normal Words. This module packages normal-word witnesses for the cleaned symbo...