English
There is a canonical (semi)ring isomorphism between the opposite ring R^op and the endomorphism ring End_R(R) given by right multiplication: a^op ↦ (x ↦ x a).
Русский
Существует каноническое изоморфизм кольца R^{op} и End_R(R), заданный правым умножением: a^{op} ↦ (x ↦ x a).
LaTeX
$$$R^{\\mathrm{op}} \\cong \\mathrm{End}_R(R),\\; a^{\\mathrm{op}} \\mapsto (x \\mapsto x a).$$$
Lean4
/-- The canonical (semi)ring isomorphism from `Rᵐᵒᵖ` to `Module.End R R` induced by the right
multiplication. -/
@[simps]
def moduleEndSelf : Rᵐᵒᵖ ≃+* Module.End R R :=
{ Module.toModuleEnd R R with
toFun := DistribMulAction.toLinearMap R R
invFun := fun f ↦ MulOpposite.op (f 1)
left_inv := mul_one
right_inv := fun _ ↦ LinearMap.ext_ring <| one_mul _ }
