Commit 2023-03-13 12:12 2196ab36

refactor(algebra/group/basic): rework lemmas on inv and neg (#17483) This PR adds the following lemma (and its additive equivalent).

theorem inv_eq_iff_eq_inv : a⁻¹ = b ↔ a = b⁻¹

and removes eq_inv_of_eq_inv, eq_inv_iff_eq_inv and inv_eq_iff_inv_eq (and their additive equivalents).