smul_dotProduct — Mathlib

English

For a scalar x, and vectors v,w, the dot product is compatible with scalar multiplication: v ⬝ᵥ x • w = x • (v ⬝ᵥ w).

Русский

Для скаляра x и векторов v, w верно: v ⬝ᵥ x • w = x • (v ⬝ᵥ w).

LaTeX

$$$ \; v \cdot (x \cdot w) = x \cdot (v \cdot w) $$$

Lean4

@[simp]
theorem smul_dotProduct [IsScalarTower R α α] (x : R) (v w : m → α) : x • v ⬝ᵥ w = x • (v ⬝ᵥ w) := by
  simp [dotProduct, Finset.smul_sum, smul_mul_assoc]

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