toMatrix_reindexRange — Mathlib

English

The matrix of the algebra map algebraMap R (Module.End R M1) x, viewed as a linear map on M1, is the diagonal (scalar) matrix with x on the diagonal.

Русский

Матрица линейного отображения алгебраического отображения algebraMap R (Module.End R M1) x равна диагональной (scalar) матрице с x на диагонали.

LaTeX

$$$\\text{toMatrix } v_1 v_1 (\\text{algebraMap } R (\\mathrm{End}_R M_1) x) = \\text{scalar}_{n}(x).$$$

Lean4

theorem toMatrix_reindexRange [DecidableEq M₁] (f : M₁ →ₗ[R] M₂) (k : m) (i : n) :
    LinearMap.toMatrix v₁.reindexRange v₂.reindexRange f ⟨v₂ k, Set.mem_range_self k⟩ ⟨v₁ i, Set.mem_range_self i⟩ =
      LinearMap.toMatrix v₁ v₂ f k i :=
  by simp_rw [LinearMap.toMatrix_apply, Basis.reindexRange_self, Basis.reindexRange_repr]

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