mathlib

f8bc097d - feat(algebra/module/linear_map): `Rᵐᵒᵖ` is isomorphic to `module.End R R` (#13931)

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.