Theorem Subgroup.commutator_top_left_eq_bot_iff_le_center

Modification history

2026-06-24 00:45
Mathlib/GroupTheory/Commutator/Basic.lean
feat(GroupTheory/IsPerfect): Grün's lemma (#39956) …
Added Subgroup.commutator_top_left_eq_bot_iff_le_centerView on Github →