Theorem Group.IsNilpotent.exists_normal_card_eq_of_dvd_card

Modification history

2026-08-31 14:42
Mathlib/GroupTheory/Nilpotent.lean
feat(GroupTheory): results on normal subgroups of nilpotent groups (#43061) …
Added Group.IsNilpotent.exists_normal_card_eq_of_dvd_cardView on Github →