coe_smul — Mathlib

English

The coe (to function) commutes with scalar multiplication: (r • p) as a function equals r • (p as a function).

Русский

Сопоставление коe с умножением на скаляр сохраняет форму: (r • p) как функция равно r • (p как функция).

LaTeX

$$$\text{Seminorm}.instFunLike .coe (instHSMul.hSMul r p) = r \cdot (\text{Seminorm}.instFunLike.coe p)$$$

Lean4

theorem coe_smul [SMul R ℝ] [SMul R ℝ≥0] [IsScalarTower R ℝ≥0 ℝ] (r : R) (p : Seminorm 𝕜 E) : ⇑(r • p) = r • ⇑p :=
  rfl

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