Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-12 14:08 9456a744

View on Github →

feat(group_theory/commutator): Prove commutator_eq_bot_iff_le_centralizer (#12598) This lemma is needed for the three subgroups lemma.

Estimated changes