smulAddHom — Mathlib

English

The map r ↦ (x ↦ r · x) is an AddMonoidHom R → End(M).

Русский

Отображение скаляра в конецоморфизм: r ↦ (x ↦ r · x) является гомоморфизмом AddMonoid.

LaTeX

$$$\\text{smulAddHom} : R \\to^+ \\mathrm{End}(M),\\quad \\text{smulAddHom}(r)(x) = r \\cdot x$$$

Lean4

/-- A convenience alias for `Module.toAddMonoidEnd` as an `AddMonoidHom`, usually to allow the
use of `AddMonoidHom.flip`. -/
def smulAddHom : R →+ M →+ M :=
  (Module.toAddMonoidEnd R M).toAddMonoidHom

Похожие утверждения