ProCGroups/NormalSubgroups.lean
1import ProCGroups.NormalSubgroups.MaximalIntersectionsAndSimpleRanks
2import ProCGroups.NormalSubgroups.PointedSumsAndSimpleQuotients
3import ProCGroups.NormalSubgroups.SimpleQuotients.Compactness
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/NormalSubgroups.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Closed normal subgroups and simple quotients
16Develops normal-subgroup frameworks, maximal intersections, simple quotient ranks, compactness arguments, and algebraic comparison theorems.
17-/