English
Let M be an m×n matrix over a nonunital semiring, v a function from a finite index l to α, e1: l ≃ m and e2: o → n. Then the row-vector resulting from v acting on the submatrix M.submatrix(e1, e2) equals the composition of the row-vector (v ∘ e1.symm) acting on M, followed by restricting via e2.
Русский
Пусть M — матрица размерности m×n над полупрямоугольной полускалярной системой, v: l→α. При отображениях e1: l ≃ m и e2: o→n верно: v ᵥ* M.submatrix(e1, e2) = (v ∘ e1.symm) ᵥ* M ∘ e2.
LaTeX
$$$\\text{Let } M \\in M_{m\\times n}(\\alpha),\\; v: L \\to \\alpha,\\; e_1: L \\simeq m,\\; e_2: o \\to n.\\quad v \\ ᵥ*\\; M_{\\lvert e_1, e_2\\rvert} = (v \\circ e_1^{-1}) ᵥ* M \\circ e_2.$$$
Lean4
theorem submatrix_vecMul_equiv [Fintype l] [Fintype m] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : l → α)
(e₁ : l ≃ m) (e₂ : o → n) : v ᵥ* M.submatrix e₁ e₂ = ((v ∘ e₁.symm) ᵥ* M) ∘ e₂ :=
funext fun _ => Eq.symm (comp_equiv_symm_dotProduct _ _ _)
