coe_smul' — Mathlib

English

The canonical representative of smul on End(A) coincides with the left smul construction smulLeft.

Русский

Канонический представитель умножения на скаляр на End(A) совпадает с конструкцией smulLeft.

LaTeX

$$$ \text{coe smul'}: \bigl( .smul : R \to+ M \to+ M \bigr) = \text{End}.smulLeft$$$

Lean4

@[simp]
theorem coe_smul' [Semiring R] [AddCommMonoid M] [Module R M] : ⇑(.smul : R →+ M →+ M) = AddMonoidHom.smulLeft :=
  rfl

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