English
Keeping around LinearEquiv’s, reindexing a matrix corresponds to pre- and post-composing mulVecLin with the induced left and right linear equivalences.
Русский
При переиндексации матрицы сохраняя линейные эквивалентности, mulVecLin переиндексированного массива равен композиции слева и справа с соответствующими линейными эквивалентностями.
LaTeX
$$mulVecLin_reindex [Fintype n] [Fintype l] (e₁ : k ≃ m) (e₂ : l ≃ n) (M : Matrix k l R) :\n (reindex e₁ e₂ M).mulVecLin =\n ↑(LinearEquiv.funCongrLeft R R e₁.symm) ∘ₗ M.mulVecLin ∘ₗ ↑(LinearEquiv.funCongrLeft R R e₂)$$
Lean4
/-- A variant of `Matrix.mulVecLin_submatrix` that keeps around `LinearEquiv`s. -/
theorem mulVecLin_reindex [Fintype n] [Fintype l] (e₁ : k ≃ m) (e₂ : l ≃ n) (M : Matrix k l R) :
(reindex e₁ e₂ M).mulVecLin =
↑(LinearEquiv.funCongrLeft R R e₁.symm) ∘ₗ M.mulVecLin ∘ₗ ↑(LinearEquiv.funCongrLeft R R e₂) :=
Matrix.mulVecLin_submatrix _ _ _
