ProCGroups.ReidemeisterSchreier.Discrete.Presentations

4 sections | 16 files | 307 declarations

This aggregate exports equality modulo normal closures, quotient-kernel presentations, presentation automation, semantic Tietze equivalences, and verified elementary Tietze scripts.

imports

Imported by

ProCGroups.ReidemeisterSchreier.Discrete

Automation

1 file | 2 declarations | 2 Macros

This module defines the small proof automation used in relator calculations: it closes elementary `RelatorEquivalent` goals and reduces normal-closure membership goals to the st...

KernelQuotient

1 file | 23 declarations | 17 Theorems | 6 Definitions

This module identifies a presented free-group kernel with its relator quotient. It packages the canonical surjection, computes its kernel, and derives quotient equivalences for ...

Relators

6 files | 106 declarations | 102 Theorems | 4 Definitions

This module defines equality modulo a relator normal closure and proves its elementary equivalence, congruence, inversion, multiplication, and quotient characterizations.

Tietze

This aggregate separates semantic presentation equivalence from syntactic transformations. The core and generator/relator operation modules construct certificates; `Tietze.Scrip...