toMatrix_one — Mathlib

English

The matrix corresponding to the identity linear map with respect to any basis equals the identity matrix; this is a direct corollary of the identity in the matrix-to-map correspondence.

Русский

Матрица, соответствующая тождественному линейному отображению относительно любого базиса, равна единичной матрице; следует из соответствия матрица-отображение.

LaTeX

$$$\\text{toMatrix } v_1 v_1 \\; \\text{id} = I.$$$

Lean4

@[simp]
theorem toMatrix_one : LinearMap.toMatrix v₁ v₁ 1 = 1 :=
  LinearMap.toMatrix_id v₁

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