English
If v is a row vector indexed by the row type, then the product v ᵥ* (fromCols B1 B2) equals the sum of the row-multiplications by B1 and B2, with the left/right embeddings: v ᵥ* fromCols B1 B2 = v ᵥ* B1 ∘ Sum.inl + v ᵥ* B2 ∘ Sum.inr.
Русский
Умножение вектор-строки на матрицу, составленную из двух блоков по столбцам, эквивалентно сумме умножений на каждый блок: v ᵥ* отCols B1 B2 = v ᵥ* B1 ∘ Sum.inl + v ᵥ* B2 ∘ Sum.inr.
LaTeX
$$$$ v ᵥ* \operatorname{fromCols}(B_1,B_2) = v ᵥ* B_1 \circ \mathrm{Sum.inl} + v ᵥ* B_2 \circ \mathrm{Sum.inr}. $$$$
Lean4
@[simp]
theorem vecMul_fromCols [Fintype m] (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) (v : m → R) :
v ᵥ* fromCols B₁ B₂ = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂) := by ext (_ | _) <;> rfl
