sum_vecMul — Mathlib

English

VecMul distributes over finite sums: vecMul(x, sum_i y_i) = sum_i vecMul(x, y_i).

Русский

VecMul распределяет по конечной сумме: vecMul(x, sum_i y_i) = sum_i vecMul(x, y_i).

LaTeX

$$$\mathrm{vecMul}(x, \sum_{i \in s} y_i) = \sum_{i \in s} \mathrm{vecMul}(x, y_i).$$$

Lean4

theorem sum_vecMul (s : Finset ι) (x : ι → (n → α)) (y : Matrix n m α) : (∑ i ∈ s, x i) ᵥ* y = ∑ i ∈ s, x i ᵥ* y :=
  by
  ext
  simp only [vecMul, sum_dotProduct, Finset.sum_apply]

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