instSMul — Mathlib

English

The scalar-multiplication action distributes through the function-application: the function part of c•f equals c times the function f.

Русский

Скалярное умножение проходит через применение функции: коэффициентная часть c•f равна c умножить на функцию f.

LaTeX

$$$\forall c:\, S,\ f:\ MultilinearMap R M_1 M_2,\; (c \cdot f) = c \cdot f$ как функция$$

Lean4

instance : SMul S (MultilinearMap R M₁ M₂) :=
  ⟨fun c f => ⟨fun m => c • f m, fun m i x y => by simp [smul_add], fun l i x d => by simp [← smul_comm x c (_ : M₂)]⟩⟩

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