English
For any Finset s and family u, v, dotProduct distributes over the finite sum: dotProduct( sum_i u_i, v ) = sum_i dotProduct( u_i, v ).
Русский
Для конечной множества s и семейства функций dotProduct распределяется над суммой: dotProduct(∑_i u_i, v) = ∑_i dotProduct(u_i, v).
LaTeX
$$$$ \operatorname{dotProduct}\bigl(\,\sum_{i \in s} u_i\, ,\; v\bigr) = \sum_{i \in s} \operatorname{dotProduct}(u_i, v). $$$$
Lean4
theorem dotProduct_sum {ι : Type*} (u : m → α) (s : Finset ι) (v : ι → (m → α)) :
u ⬝ᵥ ∑ i ∈ s, v i = ∑ i ∈ s, u ⬝ᵥ v i :=
by
simp only [dotProduct, Finset.sum_apply, Finset.mul_sum]
rw [Finset.sum_comm]
