English
Let M be m×n and N be o×p matrices over a semiring. For a finite type bijection e2: o ≃ n and a map e1: l → p, the product M.submatrix(id, e2) · N.submatrix(id, e1) equals M · N.submatrix(e2.symm, e1).
Русский
Пусть M имеет размерность m×n, N — o×p над полем (полем не обязательно коммутативным). При отображении e2: o ≃ n и e1: l → p верно: M_{submatrix,id,e2} · N_{submatrix,id,e1} = M · N_{submatrix,e2^{-1},e1}.
LaTeX
$$$\\text{Let } M \\in M_{m\\times n}(\\alpha), \\; N \\in M_{o\\times p}(\\alpha).\\; e_1: L \\to p, \\; e_2: o \\simeq n.\\quad M_{\\lvert id, e_2\\rvert} \\cdot N_{\\lvert id, e_1\\rvert} = M \\cdot N_{\\lvert e_2^{-1}, e_1\\rvert}. $$$
Lean4
@[simp]
theorem submatrix_id_mul_right [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p : Type*} (M : Matrix m n α)
(N : Matrix o p α) (e₁ : l → p) (e₂ : o ≃ n) : M.submatrix id e₂ * N.submatrix id e₁ = M * N.submatrix e₂.symm e₁ :=
by ext; simp [mul_apply, ← e₂.bijective.sum_comp]
