dotProduct_smul — Mathlib

English

The dot product commutes with scalar multiplication in a scalar-tower setting: dotProduct v (x • w) = x • dotProduct v w.

Русский

Скалярное произведение коммутирует с умножением на скаляр: dotProduct v (x • w) = x • dotProduct v w.

LaTeX

$$$ \; \text{dotProduct}(v, x \cdot w) = x \cdot \text{dotProduct}(v, w) $$$

Lean4

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

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