toFun_smul — Mathlib

English

For any scalar c from M and f in UniformFun α β, the evaluation preserves the scalar action: toFun(c • f) = c • toFun f.

Русский

Для скаляра c из M и f из UniformFun α β отображение сохраняет действие скаляра: toFun(c • f) = c • toFun f.

LaTeX

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

Lean4

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

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