Theorem commute_iff_eq

Modification history

2024-05-18 16:15
Mathlib/Algebra/Group/Commute/Defs.lean
chore: Delete `Algebra.GroupPower.Basic`, `Algebra.GroupWithZero.Bitwise` (#11855) …
Modified commute_iff_eqView on Github →
2024-02-14 08:30
Mathlib/Algebra/Group/Commute/Defs.lean
feat(Algebra/Group): Add commute_iff_eq and a few lemmas on conjugation (#9870) …
Added commute_iff_eqView on Github →