sum_mulVec — Mathlib

English

Sum of a family of matrices multiplies a vector termwise: (sum_i x_i) *ᵥ y = sum_i (x_i *ᵥ y).

Русский

Сумма семейства матриц умножает вектор построчно: (sum_i x_i) *ᵥ y = sum_i (x_i *ᵥ y).

LaTeX

$$$\left(\sum_{i} x_i\right) *ᵥ y = \sum_{i} x_i *ᵥ y$ for matrices x_i and vector y.$$

Lean4

theorem sum_mulVec (s : Finset ι) (x : ι → Matrix m n α) (y : n → α) : (∑ i ∈ s, x i) *ᵥ y = ∑ i ∈ s, x i *ᵥ y :=
  by
  ext
  simp only [mulVec, dotProduct, sum_apply, Finset.sum_mul, Finset.sum_apply]
  rw [Finset.sum_comm]

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