add_dotProduct — Mathlib

English

Dot product is linear in its left argument: dotProduct(u+v, w) = dotProduct(u,w) + dotProduct(v,w).

Русский

Скалярное произведение линейно по левому аргументу: dotProduct(u+v, w) = dotProduct(u,w) + dotProduct(v,w).

LaTeX

$$$$\operatorname{dotProduct}(u+v, w) = \operatorname{dotProduct}(u,w) + \operatorname{dotProduct}(v,w).$$$$

Lean4

@[simp]
theorem add_dotProduct : (u + v) ⬝ᵥ w = u ⬝ᵥ w + v ⬝ᵥ w := by simp [dotProduct, add_mul, Finset.sum_add_distrib]

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