English
Let v be a function on the disjoint sum m1 ⊕ m2. Then the vector multiplication of v with the block rows equals the sum of the vector multiplications with each block, with the appropriate domain embedding: v ᵥ* (A1.fromRows A2) = (v ∘ Sum.inl) ᵥ* A1 + (v ∘ Sum.inr) ᵥ* A2.
Русский
Пусть v задано на разложении m1 ⊕ m2. Тогда умножение вектор-строки на блок по строкам равно сумме умножений на каждый блок: v ᵥ* (A1.fromRows A2) = (v ∘ Sum.inl) ᵥ* A1 + (v ∘ Sum.inr) ᵥ* A2.
LaTeX
$$$$ v ᵥ* (A_1.fromRows A_2) = (v \circ \mathrm{Sum.inl}) ᵥ* A_1 + (v \circ \mathrm{Sum.inr}) ᵥ* A_2. $$$$
Lean4
@[simp]
theorem vecMul_fromRows [Fintype m₁] [Fintype m₂] (B₁ : Matrix m₁ n R) (B₂ : Matrix m₂ n R) (v : m₁ ⊕ m₂ → R) :
v ᵥ* fromRows B₁ B₂ = v ∘ Sum.inl ᵥ* B₁ + v ∘ Sum.inr ᵥ* B₂ := by simp [← sumElim_vecMul_fromRows]
