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