Endomorphism of ring over itself

Stream: Is there code for X?

[Hanting Zhang]

Do we have anything that says module.End R R ≃+* Rᵒᵖ? A subproblem is turning the right multiplication λ r s, s * r : R → R →ₗ[R] R into a R-linear map. I am almost certain we have the second because I remember using it, but it has eluded all my search :(

[Eric Wieser]

The latter looks like docs#algebra.lmul_right

[Haruhisa Enomoto]

This fact is very basic and useful (for example, for the Artin-Wedderburn structure theorem of semsimple rings), and I've just written a code for it.
I'd like this to be in mathlib, but where is the right place for it in mathlib?

[Eric Wieser]

Probably either algebra.module.linear_map or algebra/algebra/bilinearis a sensible place to put it