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]