coe_toLinearMap_one — Mathlib

English

The linear map associated to the identity equivalence is the identity linear map.

Русский

Линейное отображение, связанное с тождественной эквивалентностью, является тождественным линейным отображением.

LaTeX

$$$ (↑(1 : M \simeq_R M) : M \to_{R} M) = \mathrm{LinearMap.id} $$$

Lean4

@[simp]
theorem coe_toLinearMap_one : (↑(1 : M ≃ₗ[R] M) : M →ₗ[R] M) = LinearMap.id :=
  rfl

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