ofFun_smul — Mathlib

English

For any scalar c and f in ordinary functions, the embedding respects scalar multiplication: ofFun(c • f) = c • ofFun f.

Русский

Для скаляра c и функции f отображение ofFun сохраняет действие скаляра: ofFun(c • f) = c • ofFun f.

LaTeX

$$$\operatorname{ofFun}(c \cdot f) = c \cdot \operatorname{ofFun}(f).$$$

Lean4

@[simp]
theorem ofFun_smul {M : Type*} [SMul M β] (c : M) (f : α → β) : ofFun (c • f) = c • ofFun f :=
  rfl

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