toMatrixAlgEquiv'_apply — Mathlib

English

The i,j-entry of the matrix corresponding to a linear map f is the value of f on the j-th standard basis vector.

Русский

Элемент матрицы, соответствующей линейному отображению f, равен значению f на j-мом векторе базиса e_j.

LaTeX

$$$ f : ((n \\to R) \\to_R (n \\to R)) \\quad\\Rightarrow\\quad f(i,j) = f(\\mathbf{e}_j)i $$$

Lean4

@[simp]
theorem toMatrixAlgEquiv'_apply (f : (n → R) →ₗ[R] n → R) (i j) :
    LinearMap.toMatrixAlgEquiv' f i j = f (fun j' ↦ if j' = j then 1 else 0) i := by simp [LinearMap.toMatrixAlgEquiv']

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