Commit 2021-08-18 18:52 4e7e7df8

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]