Commit 2026-08-31 14:42 486d3e60

feat(GroupTheory): results on normal subgroups of nilpotent groups (#43061) We prove that every nontrivial normal subgroup of a nilpotent group intersects the center nontrivially (Group.IsNilpotent.inf_center_ne_bot_of_normal) and that finite nilpotent groups have normal subgroups of every possible order (Group.IsNilpotent.exists_normal_of_dvd_card).