lsmul_apply — Mathlib

English

The action of scalar multiplication on a vector space is implemented by the linear map lsmul, and evaluating it yields the expected scalar action.

Русский

Действие скалярного умножения на векторное пространство реализуется через отображение lsmul, и вычисление даёт ожидаемое действие скаляра.

LaTeX

$$$\text{lsmul}\;\; c\; x = c\cdot x$$$

Lean4

@[simp]
theorem lsmul_apply (c : R) (x : E) : lsmul 𝕜 R c x = c • x :=
  rfl

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