toMatrix_apply' — Mathlib

English

Changing the indexing of a matrix via reindexRange corresponds to the same change on the indices of the basis in the linear map; the matrix of f with reindexed bases equals the reindexed matrix of f.

Русский

Изменение индексации через reindexRange приводит к тому же изменению индексов базиса в линейном отображении; матрица f с переиндексацией равна переиндексированной матрице f.

LaTeX

$$$\\text{toMatrix}_{v_1',v_2'} f = (\\text{toMatrix}_{v_1,v_2} f)^{\\text{reindexed}}$$$

Lean4

theorem toMatrix_apply' (f : M₁ →ₗ[R] M₂) (i : m) (j : n) : LinearMap.toMatrix v₁ v₂ f i j = v₂.repr (f (v₁ j)) i :=
  LinearMap.toMatrix_apply v₁ v₂ f i j

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