Commit 2024-02-14 08:30 da3c42f7

feat(Algebra/Group): Add commute_iff_eq and a few lemmas on conjugation (#9870) This introduces some helpful, small lemmas around conjugation in groups, as well as commute_iff_eq, which removes the need to use show or unfold to get an expression of the form a * b = b * a to prove.