feat(algebra/module/linear_map): Rᵐᵒᵖ is isomorphic to `module.End …

…R R` (#13931)

This PR adds the canonical (semi)ring isomorphism from `Rᵐᵒᵖ` to
`module.End R R` for a (semi)ring `R`, given by the right multiplication.

src/algebra/module/linear_map.lean

@@ -314,6 +314,9 @@ ext $ λ x, by rw [← mul_one x, ← smul_eq_mul, f.map_smulₛₗ, g.map_smul
 theorem ext_ring_iff {σ : R →+* R} {f g : R →ₛₗ[σ] M} : f = g ↔ f 1 = g 1 :=
 ⟨λ h, h ▸ rfl, ext_ring⟩
 
+@[ext] theorem ext_ring_op {σ : Rᵐᵒᵖ →+* S} {f g : R →ₛₗ[σ] M₃} (h : f 1 = g 1) : f = g :=
+ext $ λ x, by rw [← one_mul x, ← op_smul_eq_mul, f.map_smulₛₗ, g.map_smulₛₗ, h]
+
 end
 
 /-- Interpret a `ring_hom` `f` as an `f`-semilinear map. -/
@@ -843,4 +846,24 @@ def to_module_End : S →+* module.End R M :=
   map_add' := λ f g, linear_map.ext $ add_smul _ _,
   ..distrib_mul_action.to_module_End R M }
 
+/-- The canonical (semi)ring isomorphism from `Rᵐᵒᵖ` to `module.End R R` induced by the right
+multiplication. -/
+@[simps]
+def module_End_self : Rᵐᵒᵖ ≃+* module.End R R :=
+{ to_fun := distrib_mul_action.to_linear_map R R,
+  inv_fun := λ f, mul_opposite.op (f 1),
+  left_inv := mul_one,
+  right_inv := λ f, linear_map.ext_ring $ one_mul _,
+  ..module.to_module_End R R }
+
+/-- The canonical (semi)ring isomorphism from `R` to `module.End Rᵐᵒᵖ R` induced by the left
+multiplication. -/
+@[simps]
+def module_End_self_op : R ≃+* module.End Rᵐᵒᵖ R :=
+{ to_fun := distrib_mul_action.to_linear_map _ _,
+  inv_fun := λ f, f 1,
+  left_inv := mul_one,
+  right_inv := λ f, linear_map.ext_ring_op $ mul_one _,
+  ..module.to_module_End _ _ }
+
 end module