English
Let e₂ be an equivalence o ≃ n. Then M.submatrix e₁ e₂ · N.submatrix e₂ e₃ = (M N).submatrix e₁ e₃, expressing compatibility of submatrices with equivalences of indices.
Русский
Пусть e₂: o ≃ n. Тогда M.submatrix e₁ e₂ · N.submatrix e₂ e₃ = (M N).submatrix e₁ e₃, выражая совместимость подматриц с эквивалентностями индексов.
LaTeX
$$M.submatrix e₁ e₂ · N.submatrix e₂ e₃ = (M N).submatrix e₁ e₃$$
Lean4
@[simp]
theorem submatrix_mul_equiv [Fintype n] [Fintype o] [AddCommMonoid α] [Mul α] {p q : Type*} (M : Matrix m n α)
(N : Matrix n p α) (e₁ : l → m) (e₂ : o ≃ n) (e₃ : q → p) :
M.submatrix e₁ e₂ * N.submatrix e₂ e₃ = (M * N).submatrix e₁ e₃ :=
(submatrix_mul M N e₁ e₂ e₃ e₂.bijective).symm
