English
Given M ∈ M_{m×n}(α) and N ∈ M_{n×p}(α) with index maps e₁,e₂,e₃ and a bijection e₂ between n and o, the submatrix of MN equals the product of the corresponding submatrices: (MN).submatrix e₁ e₃ = M.submatrix e₁ e₂ · N.submatrix e₂ e₃.
Русский
Пусть M ∈ M_{m×n}(α) и N ∈ M_{n×p}(α) с отображениями индексов и биекцией e₂ между n и o; тогда подматрица произведения MN равна произведению соответствующих подматриц.
LaTeX
$$$(MN).submatrix e₁ e₃ = M.submatrix e₁ e₂ · N.submatrix e₂ e₃$$$
Lean4
theorem submatrix_mul [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p q : Type*} (M : Matrix m n α)
(N : Matrix n p α) (e₁ : l → m) (e₂ : o → n) (e₃ : q → p) (he₂ : Function.Bijective e₂) :
(M * N).submatrix e₁ e₃ = M.submatrix e₁ e₂ * N.submatrix e₂ e₃ :=
ext fun _ _ => (he₂.sum_comp _).symm
