mathlib3

e6c787fe - feat(algebra/opposites): add `has_scalar (opposite α) α` instances (#7630)

feat(algebra/opposites): add `has_scalar (opposite α) α` instances (#7630) The action is defined as: ```lean lemma op_smul_eq_mul [monoid α] {a a' : α} : op a • a' = a' * a := rfl ``` We have a few of places in the library where we prove things about `r • b`, and then extract a proof of `a * b = a • b` for free. However, we have no way to do this for `b * a` right now unless multiplication is commutative. By adding this action, we have `b * a = op a • b` so in many cases could reuse the smul lemma. This instance does not create a diamond: ```lean -- the two paths to `mul_action (opposite α) (opposite α)` are defeq example [monoid α] : monoid.to_mul_action (opposite α) = opposite.mul_action α (opposite α) := rfl ``` [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Right.20multiplication.20as.20a.20mul_action/near/239012917)