English
Reindexing of rows and columns induces a conjugation of the associated linear map by the corresponding linear equivalences.
Русский
Переиндексация строк и столбцов порождает сопряжение соответствующего линейного отображения соответствующими линейными эквивалентностями.
LaTeX
$$$ \\mathrm{toLin'}\\bigl(\\mathrm{reindex}\\, e_1\\, e_2\\ M\\bigr) = \\mathrm{funCongrLeft}_{R,R}(e_1^{\\mathrm{symm}}) \\circ \\mathrm{toLin'}(M) \\circ \\mathrm{funCongrLeft}_{R,R}(e_2) $$$
Lean4
/-- A variant of `Matrix.toLin'_submatrix` that keeps around `LinearEquiv`s. -/
theorem toLin'_reindex [Fintype l] [DecidableEq l] (e₁ : k ≃ m) (e₂ : l ≃ n) (M : Matrix k l R) :
Matrix.toLin' (reindex e₁ e₂ M) =
↑(LinearEquiv.funCongrLeft R R e₁.symm) ∘ₗ (Matrix.toLin' M) ∘ₗ ↑(LinearEquiv.funCongrLeft R R e₂) :=
Matrix.mulVecLin_reindex _ _ _
