Yamaguchi Lean 4 Library
ProCGroups.Presentations
ProCGroups/Presentations

ProCGroups.Presentations

2 sections | 5 files | 214 declarations

This module develops finite quotient, subgroup, free pro-\(C\), generation, and cardinal-invariant constructions for profinite and pro-\(C\) groups.

Profinite

1 files | 32 declarations | 18 Theorem | 11 Definition | 1 Abbreviation | 1 Structure | 1 Instance
The closed normal subgroup generated by a set of profinite relators.

SchreierTietze

4 files | 182 declarations | 81 Theorem | 70 Definition | 11 Abbreviation | 20 Structure
Wrapper for the `ProCGroups.Presentations.SchreierTietze` folder.