English
For bijection e1: n ≃ o and e2: l → o, and M ∈ M_{m×n}(α), we have M * (1_{o×o} submatrix e1 e2) = submatrix M id (e1.symm ∘ e2).
Русский
Пусть e1: n ≃ o и e2: l → o, M ∈ M_{m×n}(α). Тогда: M · (1_{o×o} с подматрицей e1,e2) = submatrix M id (e1^{-1} ∘ e2).
LaTeX
$$$\\text{Let } M \\in M_{m\\times n}(\\alpha), \\; (1: M_{o\\times o})_{submatrix e1,e2} \\in M_{l\\times p}(\\alpha).\\quad M \\cdot (1)_{submatrix e1,e2} = (M)_{submatrix id,e1^{-1} \\circ e2}.$$$
Lean4
theorem mul_submatrix_one [Fintype n] [Finite o] [NonAssocSemiring α] [DecidableEq o] (e₁ : n ≃ o) (e₂ : l → o)
(M : Matrix m n α) : M * (1 : Matrix o o α).submatrix e₁ e₂ = submatrix M id (e₁.symm ∘ e₂) :=
by
cases nonempty_fintype o
let A := M.submatrix id e₁.symm
have : M = A.submatrix id e₁ := by
simp only [A, submatrix_submatrix, Function.comp_id, submatrix_id_id, Equiv.symm_comp_self]
rw [this, submatrix_mul_equiv]
simp only [A, Matrix.mul_one, submatrix_submatrix, Function.comp_id, submatrix_id_id, Equiv.symm_comp_self]
