mathlib

2196ab36 - refactor(algebra/group/basic): rework lemmas on inv and neg (#17483)

refactor(algebra/group/basic): rework lemmas on inv and neg (#17483) This PR adds the following lemma (and its additive equivalent). ```lean 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).