entryLinearMap_comp_mapMatrix — Mathlib

English

For a linear map f: R→S, the matrix-entry linear map composed with the induced matrix map equals the induced linear map composed with the matrix-entry map.

Русский

Для линейного отображения f: R→S композиция линейного отображения на элементы матрицы и индуцированного отображения матриц эквивалентна композиции индуцированного отображения на элементы матрицы и линейному отображению на коэффициентах.

LaTeX

$$$(\\text{entryLinearMap } S \\_\\ _ i j).\\circ (f.mapMatrix) = f.\\circ (\\text{entryLinearMap } R \\_\\ _ i j)$$$

Lean4

@[simp]
theorem entryLinearMap_comp_mapMatrix (f : α →ₛₗ[σᵣₛ] β) (i : m) (j : n) :
    (entryLinearMap S _ i j).comp f.mapMatrix = f.comp (entryLinearMap R _ i j) :=
  rfl

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