mathlib3

59643439 - feat(data/equiv): define `mul_equiv_class` (#10760)

feat(data/equiv): define `mul_equiv_class` (#10760) This PR defines a class of types of multiplicative (additive) equivalences, along the lines of #9888. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>