Source: ProCGroups.ProC.MaximalQuotients
1import ProCGroups.ProC.MaximalQuotients.Definitions
2import ProCGroups.ProC.MaximalQuotients.ResidualCore
3import ProCGroups.ProC.MaximalQuotients.UniversalProperty
5/-!
6# Maximal pro-\(C\) quotients
8This aggregate exports the universal-property definition of a maximal pro-\(C\) quotient, its
9construction from the intersection of all admissible kernels, and the resulting factorization
10theorems.
11-/