Source: ProCGroups.NormalSubgroups.SimpleQuotients
1import ProCGroups.NormalSubgroups.SimpleQuotients.Algebraic
2import ProCGroups.NormalSubgroups.SimpleQuotients.Compactness
3import ProCGroups.NormalSubgroups.SimpleQuotients.FiniteIntersections
5/-!
6# Simple quotients
8This aggregate module exposes the algebraic dichotomy for subgroups above a simple-quotient
9kernel, its finite-intersection form, and the compactness argument for arbitrary intersections.
10-/