mathlib3

4e7e7df8 - feat(algebra/monoid_algebra): add_monoid_algebra.op_{add,ring}_equiv (#8536)

feat(algebra/monoid_algebra): add_monoid_algebra.op_{add,ring}_equiv (#8536) Transport an opposite `add_monoid_algebra` to the algebra over the opposite ring. On the way, - provide API lemma `mul_equiv.inv_fun_eq_symm {f : M ≃* N} : f.inv_fun = f.symm` and the additive version - generalize simp lemmas `equiv_to_opposite_(symm_)apply` to `equiv_to_opposite_(symm_)coe` - tag `map_range.(add_)equiv_symm` with `[simp] Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>