dotProduct_sub — Mathlib

English

Another formulation of dot product distributivity with subtraction: u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w.

Русский

Еще одно формулирование распределности скалярного произведения над разностью: u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w.

LaTeX

$$$ u \cdot (v - w) = u \cdot v - u \cdot w $$$

Lean4

@[simp]
theorem dotProduct_sub : u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w := by simp [sub_eq_add_neg]

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