Yamaguchi Lean 4 Library
ProCGroups.ProC.Subgroups
ProCGroups/ProC/Subgroups

ProCGroups.ProC.Subgroups

2 sections | 2 files | 17 declarations

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

Closed

1 files | 11 declarations | 11 Theorem
A closed subgroup of a pro-\(C\) group is pro-\(C\).

Products

1 files | 6 declarations | 6 Theorem
A closed subgroup of a product of profinite groups is profinite. This is a direct theorem around the already-completed pi and closed-subgroup permanence lemmas.