coe_smul — Mathlib

English

For r ∈ R and p ∈ NonarchAddGroupSeminorm E, the underlying function of r • p is r times the underlying function of p.

Русский

Для r ∈ R и p ∈ NonarchAddGroupSeminorm E, базовая функция r • p равна r умножению базовой функции p.

LaTeX

$$$ (r \cdot p) = r \cdot (p) $ as functions, i.e., (r • p)(x) = r • p(x)$$

Lean4

@[simp, norm_cast]
theorem coe_smul (r : R) (p : NonarchAddGroupSeminorm E) : ⇑(r • p) = r • ⇑p :=
  rfl

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