English
End_R(M) is a semiring with addition defined pointwise and multiplication defined by composition; in particular, 1 acts as the identity and the usual distributive laws hold.
Русский
End_R(M) является полукольцом: сложение — покоординатное, умножение — композиция; 1 — единица; выполняются обычные тождества распределительности.
LaTeX
$$$ \mathrm{End}_R(M) \text{ is a semiring with } (f \cdot g) = f \circ g \text{ and } 0,1 \text{ as standard.}$$$
Lean4
instance instSemiring : Semiring (Module.End R M)
where
__ := AddMonoidWithOne.unary
__ := instMonoid
__ := addCommMonoid
mul_zero := comp_zero
zero_mul := zero_comp
left_distrib := fun _ _ _ ↦ comp_add _ _ _
right_distrib := fun _ _ _ ↦ add_comp _ _ _
natCast := fun n ↦ n • (1 : M →ₗ[R] M)
natCast_zero := zero_smul ℕ (1 : M →ₗ[R] M)
natCast_succ := fun n ↦ AddMonoid.nsmul_succ n (1 : M →ₗ[R] M)
