smul_of — Mathlib

English

The embedding preserves scalar multiplication: for any r in R and f: m → n → α, r • of f = of (r • f).

Русский

Встраивание сохраняет скалярное умножение: для любого r в R и функции f: m → n → α выполняется r • of f = of (r • f).

LaTeX

$$$ r \\cdot \\mathrm{of}(f) = \\mathrm{of}(r \\cdot f) $$$

Lean4

@[simp]
theorem smul_of [SMul R α] (r : R) (f : m → n → α) : r • of f = of (r • f) :=
  rfl

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