toLinAlgEquiv_one — Mathlib

English

With v1 as a basis, the matrix representing the identity map is the identity matrix; i.e., Matrix.toLinAlgEquiv v1 1 = LinearMap.id.

Русский

При базисе v1 матрица, представляющая единичное отображение, является тождественной—Matrix.toLinAlgEquiv v1 1 = LinearMap.id.

LaTeX

$$$\mathrm{toLinAlgEquiv}_{v_1}(1) = \mathrm{LinearMap.id}$$$

Lean4

theorem toLinAlgEquiv_one : Matrix.toLinAlgEquiv v₁ 1 = LinearMap.id := by
  rw [← LinearMap.toMatrixAlgEquiv_id v₁, Matrix.toLinAlgEquiv_toMatrixAlgEquiv]

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