Theorem Subgroup.commutator_eq_bot_iff_le_centralizer

Modification history

2023-07-27 07:08

Mathlib/GroupTheory/Commutator.lean

chore(GroupTheory): forward-port leanprover-community/mathlib#18965 (#6147)

Modified Subgroup.commutator_eq_bot_iff_le_centralizer View on Github →

2023-02-11 15:32

Mathlib/GroupTheory/Commutator.lean

feat: port GroupTheory.Commutator (#2143)

Added Subgroup.commutator_eq_bot_iff_le_centralizer View on Github →