ProCGroups.NormalSubgroups.maximal_normal_intersection_simple_quotient
A maximal normal subgroup gives a simple quotient.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped Cardinal
namespace ProCGroups.NormalSubgroups
universe uLean source · statement
theorem maximal_normal_intersection_simple_quotient
{G : Type u} [Group G] (M : Subgroup G) [M.Normal]
(hproper : M ≠ ⊤)
(hmax : ∀ N : Subgroup G, N.Normal → M < N → N = ⊤) :
IsSimpleGroup (G ⧸ M)