English
Each element of the monoid S defines a linear endomorphism of M, yielding a monoid homomorphism S → End_R(M) given by s ↦ (m ↦ s · m).
Русский
Каждый элемент моноида S определяет линейное эндоморфизм на M, образуя гомоморфизм S → End_R(M), где s ↦ (m ↦ s · m).
LaTeX
$$$\\mathrm{toModuleEnd}: S \\to \\mathrm{End}_R(M),\\; \\mathrm{toModuleEnd}(s)(m) = s\\cdot m,\\; \\mathrm{toModuleEnd}(st) = \\mathrm{toModuleEnd}(s) \\circ\\mathrm{toModuleEnd}(t),\\; \\mathrm{toModuleEnd}(1) = \\mathrm{id}_M.$$$
Lean4
/-- Each element of the semiring defines a module endomorphism.
This is a stronger version of `DistribMulAction.toModuleEnd`. -/
@[simps]
def toModuleEnd : S →+* Module.End R M :=
{ DistribMulAction.toModuleEnd R M with
toFun := DistribMulAction.toLinearMap R M
map_zero' := LinearMap.ext <| zero_smul S
map_add' := fun _ _ ↦ LinearMap.ext <| add_smul _ _ }
