English
The action of R on M induces a RingHom R → End(M) sending r to the endomorphism x ↦ r · x.
Русский
Действие R на M порождает гомоморфизм колец R → End(M), отправляющий r в эндоморфизм x ↦ r · x.
LaTeX
$$$\\text{toAddMonoidEnd } : R \\to^+ \\mathrm{End}(M),\\quad \\text{toAddMonoidEnd}(r)(x) = r \\cdot x$$$
Lean4
/-- `(•)` as an `AddMonoidHom`.
This is a stronger version of `DistribMulAction.toAddMonoidEnd` -/
@[simps! apply_apply]
def toAddMonoidEnd : R →+* AddMonoid.End M :=
{
DistribMulAction.toAddMonoidEnd R
M with
map_zero' := AddMonoidHom.ext fun r => by simp
map_add' x y := AddMonoidHom.ext fun r => by simp [(AddMonoidHom.add_apply), add_smul] }
