coe_smul — Mathlib

English

The coercion respects scalar multiplication: the underlying function of m • f equals m times the underlying function of f.

Русский

Коэрция сохраняет скалярное умножение: базовая функция m • f равна m • f.

LaTeX

$$toFun(m • f) = m • toFun(f)$$

Lean4

@[simp]
theorem coe_smul {M : Type*} [Zero R] [SMulZeroClass M R] [ContinuousConstSMul M R] (m : M) (f : C(X, R)₀) :
    ⇑(m • f) = m • f :=
  rfl

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