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)

Author: eric-wieser

src/algebra/module/opposites.lean

@@ -16,7 +16,28 @@ cycles.
 namespace opposite
 universes u v
 
-variables (R : Type u) {M : Type v} [semiring R] [add_comm_monoid M] [module R M]
+variables (R : Type u) {M : Type v}
+
+/-- Like `mul_zero_class.to_smul_with_zero`, but multiplies on the right. -/
+instance mul_zero_class.to_opposite_smul_with_zero [mul_zero_class R] :
+  smul_with_zero (opposite R) R :=
+{ smul := λ c x, x * c.unop,
+  smul_zero := λ x, zero_mul _,
+  zero_smul := mul_zero }
+
+/-- Like `monoid_with_zero.to_mul_action_with_zero`, but multiplies on the right. -/
+instance monoid_with_zero.to_opposite_mul_action_with_zero [monoid_with_zero R] :
+  mul_action_with_zero (opposite R) R :=
+{ ..mul_zero_class.to_opposite_smul_with_zero R,
+  ..monoid.to_opposite_mul_action R }
+
+/-- Like `semiring.to_module`, but multiplies on the right. -/
+instance semiring.to_opposite_module [semiring R] : module (opposite R) R :=
+{ smul_add := λ r x y, add_mul _ _ _,
+  add_smul := λ r s x, mul_add _ _ _,
+  ..mul_zero_class.to_opposite_smul_with_zero R }
+
+variables [semiring R] [add_comm_monoid M] [module R M]
 
 /-- `opposite.distrib_mul_action` extends to a `module` -/
 instance : module R (opposite M) :=

src/algebra/opposites.lean

@@ -186,6 +186,18 @@ instance (R : Type*) [monoid R] [add_monoid α] [distrib_mul_action R α] :
   smul_zero := λ r, unop_injective $ smul_zero r,
   ..opposite.mul_action α R }
 
+/-- Like `monoid.to_mul_action`, but multiplies on the right. -/
+instance monoid.to_opposite_mul_action [monoid α] : mul_action (opposite α) α :=
+{ smul := λ c x, x * c.unop,
+  one_smul := mul_one,
+  mul_smul := λ x y r, (mul_assoc _ _ _).symm }
+
+-- The above instance does not create an unwanted diamond, the two paths to
+-- `mul_action (opposite α) (opposite α)` are defeq.
+example [monoid α] : monoid.to_mul_action (opposite α) = opposite.mul_action α (opposite α) := rfl
+
+lemma op_smul_eq_mul [monoid α] {a a' : α} : op a • a' = a' * a := rfl
+
 @[simp] lemma op_zero [has_zero α] : op (0 : α) = 0 := rfl
 @[simp] lemma unop_zero [has_zero α] : unop (0 : αᵒᵖ) = 0 := rfl