dotProduct_add — Mathlib

English

Reiterating associativity in the dot product setting: the mixed sums commute and associate as in Finite sums.

Русский

Повторная формулировка ассоциативности в контексте скалярного произведения: вложенные суммы можно переставлять и объединять как в конечных суммах.

LaTeX

$$$$\sum_{j} \left(\sum_{i} u(i) \; v_{i j}\right) w(j) = \sum_{i} u(i) \left(\sum_{j} v_{i j} \; w(j)\right).$$$$

Lean4

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

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