dualMap_symm — Mathlib

English

For a linear equivalence f: M1 ≃ M2, the dual map commutes with taking inverses: (LinearEquiv.dualMap f).symm = LinearEquiv.dualMap f.symm.

Русский

Для линейного эквивалента f: M1 ≃ M2 дуальное отображение коммутирует с взятием обратного: (dualMap f)^{-1} = dualMap(f^{-1}).

LaTeX

$$$$ (\\mathrm{LinearEquiv.dualMap}\\ f)^{\\mathrm{symm}} = \\mathrm{LinearEquiv.dualMap}\\ f^{\\mathrm{symm}}. $$$$

Lean4

@[simp]
theorem dualMap_symm {f : M₁ ≃ₗ[R] M₂} : (LinearEquiv.dualMap f).symm = LinearEquiv.dualMap f.symm :=
  rfl

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