toMatrixAlgEquiv'_id

Mathlib.LinearAlgebra.Matrix.ToLin

URI: https://scilib.ai/kg/mathlib#LinearMap.toMatrixAlgEquiv'_id

English

The matrix corresponding to the identity linear map is the identity matrix.

Русский

Матрица тождественного отображения равна единичной матрице.

LaTeX

$$$ \\mathrm{toMatrixAlgEquiv'}(\\mathrm{id}) = I_n $$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru