mulVecLin_submatrix — Mathlib

English

Given a matrix M with index maps f1 and e2, the mulVecLin of the submatrix equals the composition of the original mulVecLin with left and right index-change maps.

Русский

Для подматрицы с индексными отображениями f1 и e2 выполняется выражение: mulVecLin(submatrix) = left ∘ M.mulVecLin ∘ right.

LaTeX

$$(M.submatrix f₁ e₂).mulVecLin = (funLeft R R f₁) ∘ₗ M.mulVecLin ∘ₗ (funLeft R R e₂.symm)$$

Lean4

theorem mulVecLin_submatrix [Fintype n] [Fintype l] (f₁ : m → k) (e₂ : n ≃ l) (M : Matrix k l R) :
    (M.submatrix f₁ e₂).mulVecLin = funLeft R R f₁ ∘ₗ M.mulVecLin ∘ₗ funLeft _ _ e₂.symm :=
  LinearMap.ext fun _ ↦ submatrix_mulVec_equiv _ _ _ _

Похожие утверждения