Yamaguchi Lean 4 Library
Homepage
Source: ProCGroups.ProC.Subgroups
ProCGroups
/
ProC
/
Subgroups
/
Source
Source: ProCGroups.ProC.Subgroups
1
import
ProCGroups.ProC.Subgroups.Closed
2
import
ProCGroups.ProC.Subgroups.Products
3
4
/-!
5
# Subgroups and products of pro-\(C\) groups
6
7
This aggregate exports inheritance of pro-\(C\) structure by closed subgroups and extensions,
8
together with product and subdirect-product constructions.
9
-/