English
If B1 and B2 are matrices and v1, v2 are index functions, then summing the vector-multiplications over the mixed sum equals the sum of the separate multiplications: Sum.elim v1 v2 ᵥ* fromRows B1 B2 = v1 ᵥ* B1 + v2 ᵥ* B2.
Русский
Пусть B1 и B2 — матрицы, а v1, v2 — функции индексов; тогда сумма умножений вектор-строк по сумме Sum.elim равна сумме отдельных умножений: Sum.elim v1 v2 ᵥ* fromRows B1 B2 = v1 ᵥ* B1 + v2 ᵥ* B2.
LaTeX
$$$$ \operatorname{Sum.elim} v_1 v_2 ᵥ* \operatorname{fromRows}(B_1,B_2) = v_1 ᵥ* B_1 + v_2 ᵥ* B_2. $$$$
Lean4
theorem sumElim_vecMul_fromRows [Fintype m₁] [Fintype m₂] (B₁ : Matrix m₁ n R) (B₂ : Matrix m₂ n R) (v₁ : m₁ → R)
(v₂ : m₂ → R) : Sum.elim v₁ v₂ ᵥ* fromRows B₁ B₂ = v₁ ᵥ* B₁ + v₂ ᵥ* B₂ :=
by
ext
simp [Matrix.vecMul, fromRows, dotProduct]
