toMatrix'_id — Mathlib

English

The linear equivalence toLin' sends the identity matrix to the identity map.

Русский

Линейное эквивалентное отображение toLin' отправляет единичную матрицу в тождественное отображение.

LaTeX

$$theorem toLin'_one : Matrix.toLin' (1 : Matrix n n R) = LinearMap.id$$

Lean4

@[simp]
theorem toMatrix'_id : LinearMap.toMatrix' (LinearMap.id : (n → R) →ₗ[R] n → R) = 1 :=
  by
  ext
  rw [Matrix.one_apply, LinearMap.toMatrix'_apply, id_apply]

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