dualMap_refl — Mathlib

English

The dual map of a reflection (identity linear equivalence) is the reflection on the dual spaces: (id_R M)^\ast = id_R (M^*).

Русский

Дуальное отображение тождественного линейного эквивалента равно тождественному отображению на дуальном пространстве: id^\ast = id.

LaTeX

$$$$ (\\mathrm{LinearEquiv.refl}\\ _R\ \\, M)^{\\ast} = \\mathrm{LinearEquiv.refl}\\ _R\\ (M^*). $$$$

Lean4

@[simp]
theorem dualMap_refl : (LinearEquiv.refl R M₁).dualMap = LinearEquiv.refl R (Dual R M₁) :=
  by
  ext
  rfl

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