mathlib3
9456a744 - feat(group_theory/commutator): Prove `commutator_eq_bot_iff_le_centralizer` (#12598)

Commit

3 years ago

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

Author

tb65536

Parents