instSMul — Mathlib

English

The underlying function of the scaled map r • f equals r times the underlying function of f.

Русский

Базовая функция масштабированного отображения r•f равна r умноженному на базовую функцию f.

LaTeX

$$$ \text{coe}(r \cdot f) = r \cdot \text{coe}(f) $$$

Lean4

instance instSMul [Zero β] {R : Type*} [Zero R] [SMulWithZero R β] [ContinuousConstSMul R β] : SMul R C₀(α, β) :=
  ⟨fun r f => ⟨r • f, by simpa [smul_zero] using (zero_at_infty f).const_smul r⟩⟩

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