English
The linear map corresponding to a submatrix equals the composition of left and right pre/post processing maps with the linear map of the original matrix.
Русский
Линейное отображение, соответствующее подматрице, равняется композиции соответствующих линейных отображений слева и справа с линейным отображением исходной матрицы.
LaTeX
$$$ \\mathrm{toLin'}\\bigl(M_{\\text{submatrix}}\\bigr) = \\mathrm{funLeft}_{R,R}(f_1) \\circ \\mathrm{toLin'}(M) \\circ \\mathrm{funLeft}_{R,R}(e_2^{\\mathrm{symm}}) $$$
Lean4
@[simp]
theorem toLin'_submatrix [Fintype l] [DecidableEq l] (f₁ : m → k) (e₂ : n ≃ l) (M : Matrix k l R) :
Matrix.toLin' (M.submatrix f₁ e₂) = funLeft R R f₁ ∘ₗ (Matrix.toLin' M) ∘ₗ funLeft _ _ e₂.symm :=
Matrix.mulVecLin_submatrix _ _ _
