Yamaguchi Lean 4 Library
ProCGroups.Presentations.SchreierTietze
ProCGroups/Presentations/SchreierTietze

ProCGroups.Presentations.SchreierTietze

3 sections | 3 files | 182 declarations

Wrapper for the ProCGroups.Presentations.SchreierTietze folder.

Data

1 files | 63 declarations | 22 Theorem | 32 Definition | 9 Structure
The presentation map to an open-subgroup target after a proposed Schreier source maps into the source preimage.

Relators

1 files | 110 declarations | 52 Theorem | 36 Definition | 11 Abbreviation | 11 Structure
The relator set represented by an indexed family. This is the profinite analogue of the double-prime relator-family notation used in Reidemeister--Schreier/Tietze arguments.

Restricted

1 files | 9 declarations | 7 Theorem | 2 Definition
The inverse image in a presentation source of a subgroup of the target.