real_smul_ofReal — Mathlib

English

The scalar multiplication by a real number on an element of K coincides with multiplication by the real as an element of K: r • (x : K) = (r : K) * (x : K).

Русский

Умножение на вещественный скаляр на элементе K совпадает с умножением в K на соответствующий множитель: r • (x : K) = (r : K) · (x : K).

LaTeX

$$$\forall r,x:\n\mathbb{R},\ r \cdot (x : K) = (r : K) * (x : K)$$$

Lean4

@[simp, norm_cast, rclike_simps]
theorem real_smul_ofReal (r x : ℝ) : r • (x : K) = (r : K) * (x : K) :=
  real_smul_eq_coe_mul _ _

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