flip — Mathlib

English

For x ∈ M, the element p.toDualRight.symm.dualMap (p.toDualLeft x) equals the evaluation functional Dual.eval on x.

Русский

Для каждого x ∈ M элемент p.toDualRight.symm.dualMap (p.toDualLeft x) равен функционалу оценки на x.

LaTeX

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

Lean4

/-- Given a perfect pairing between `M` and `N`, we may interchange the roles of `M` and `N`. -/
@[deprecated LinearMap.IsPerfPair.flip (since := "2025-05-27")]
protected def flip : PerfectPairing R N M
    where
  toLinearMap := p.toLinearMap.flip
  bijective_left := p.bijective_right
  bijective_right := p.bijective_left

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