toDualRight_symm_toDualLeft — Mathlib

English

The equality p.toDualRight.symm.dualMap (p.toDualLeft x) = Dual.eval R M x holds for all x ∈ M.

Русский

Справедливое равенство: p.toDualRight.symm.dualMap (p.toDualLeft x) = Dual.eval R M x для всех x ∈ M.

LaTeX

$$$p.toDualRight.symm.dualMap (p.toDualLeft x) = Dual.eval R M x$$$

Lean4

@[deprecated "No replacement" (since := "2025-05-27")]
theorem toDualRight_symm_toDualLeft (x : M) : p.toDualRight.symm.dualMap (p.toDualLeft x) = Dual.eval R M x :=
  by
  ext f
  simp only [LinearEquiv.dualMap_apply, Dual.eval_apply]
  exact toDualLeft_of_toDualRight_symm p x f

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