entryLinearMap_comp_mapMatrix — Mathlib

English

For every i, j, taking the (i, j)-entry after applying the matrix map f.mapMatrix is the same as applying f to the (i, j)-entry of the original matrix.

Русский

Для любых индексов i, j взятие (i, j)-го элемента после применения отображения на матрицах f.mapMatrix совпадает с применением f к исходному (i, j)-элементу матрицы.

LaTeX

$$$\operatorname{entry}_{ij}((f.mapMatrix)(M)) = f(\operatorname{entry}_{ij}(M))$ for all i,j.$$

Lean4

theorem entryLinearMap_comp_mapMatrix (f : α ≃ₛₗ[σᵣₛ] β) (i : m) (j : n) :
    (entryLinearMap S _ i j).comp f.mapMatrix.toLinearMap = f.toLinearMap.comp (entryLinearMap R _ i j) := by
  simp only [mapMatrix_toLinearMap, LinearMap.entryLinearMap_comp_mapMatrix]

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