toMatrix'_one — Mathlib

English

The matrix corresponding to the identity linear map on R^n is the n-by-n identity matrix.

Русский

Матрица тождественного линейного отображения на пространстве R^n равна идентичной n×n матрице.

LaTeX

$$$ \\operatorname{toMatrix'}\\left(\\mathrm{Id}_{(n \\to R)}\\right) = I_n $$$

Lean4

@[simp]
theorem toMatrix'_one : LinearMap.toMatrix' (1 : (n → R) →ₗ[R] n → R) = 1 :=
  LinearMap.toMatrix'_id

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