Theorem Group.IsNilpotent.center_ne_bot

Modification history

2026-08-31 14:42
Mathlib/GroupTheory/Nilpotent.lean
feat(GroupTheory): results on normal subgroups of nilpotent groups (#43061) …
Modified Group.IsNilpotent.center_ne_botView on Github →
2026-06-02 11:20
Mathlib/GroupTheory/Nilpotent.lean
feat(GroupTheory/Nilpotent): a nontrivial nilpotent group has a nontrivial center (#39950) …
Added Group.IsNilpotent.center_ne_botView on Github →