English
For Fintype m, Finite o, Nonassociative semiring α, and e1: n ≃ o, e2: l→o, M ∈ M_{m×n}(α), the product (1)submatrix e1 e2 times M equals submatrix M id (e1.symm ∘ e2).
Русский
Пусть e1: n ≃ o, e2: l → o; Tогда: (1)_{submatrix e1,e2} · M = M_{submatrix e1^{-1} ∘ e2, id}.
LaTeX
$$$\\text{Let } M \\in M_{m\\times n}(\\alpha),\\; (1)_{submatrix e1,e2} \\in M_{o\\times o}(\\alpha).\\quad (1)_{submatrix e1,e2} \\cdot M = M_{submatrix e2^{-1} \\circ e1, id}.$$$
Lean4
theorem one_submatrix_mul [Fintype m] [Finite o] [NonAssocSemiring α] [DecidableEq o] (e₁ : l → o) (e₂ : m ≃ o)
(M : Matrix m n α) : ((1 : Matrix o o α).submatrix e₁ e₂) * M = submatrix M (e₂.symm ∘ e₁) id :=
by
cases nonempty_fintype o
let A := M.submatrix e₂.symm id
have : M = A.submatrix e₂ id := 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.one_mul, submatrix_submatrix, Function.comp_id, submatrix_id_id, Equiv.symm_comp_self]
