Yamaguchi Lean 4 Library
ProCGroups.FreeProducts
ProCGroups/FreeProducts

ProCGroups.FreeProducts

2 sections | 2 files | 168 declarations

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

Concrete

1 files | 70 declarations | 37 Theorem | 20 Definition | 2 Abbreviation | 1 Structure | 10 Instance
The abstract group underlying the binary free product of the two factors.

UniversalProperty

1 files | 98 declarations | 71 Theorem | 20 Definition | 7 Structure
Binary free products, expressed through the usual universal property.