dualMap_id — Mathlib

English

The dual map of the identity linear map is the identity on the dual space: id^* = id.

Русский

Дуальное отображение тождественного отображения равно тождественному отображению на дуальном пространстве: id^* = id.

LaTeX

$$$$ (\\mathrm{id}_M)^* = \\mathrm{id}_{M^*}. $$$$

Lean4

@[simp]
theorem dualMap_id : (LinearMap.id : M₁ →ₗ[R] M₁).dualMap = LinearMap.id :=
  by
  ext
  rfl

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