smulLeft — Mathlib

English

Left scalar multiplication by a monoid M induces an additive monoid homomorphism M →+ End(A) given by c ↦ (a ↦ c • a).

Русский

Левое скалярное умножение моноида M порождает гомоморфизм AddMonoidHom M →+ End(A), $c \mapsto (a \mapsto c • a)$.

LaTeX

$$$ \text{smulLeft} : M \to^+ \mathrm{End}(A) \quad c \mapsto (a \mapsto c \cdot a) $$$

Lean4

/-- Scalar multiplication on the left as an additive monoid homomorphism. -/
@[simps! -fullyApplied]
protected def smulLeft [Monoid M] [AddMonoid A] [DistribMulAction M A] (c : M) : A →+ A :=
  DistribMulAction.toAddMonoidHom _ c

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