toDualRight — Mathlib

English

The pairing induces a linear isomorphism N ≃ₗ[R] Dual R M, i.e., N is isomorphic to the dual of M.

Русский

Пара образует линейное эквивалентное отображение N ≃ₗ[R] Dual R M; N изоморфно Dual R M.

LaTeX

$$$N \cong_R \operatorname{Dual} R M$$$

Lean4

/-- The linear equivalence from `N` to `Dual R M` induced by a perfect pairing. -/
@[deprecated LinearMap.toPerfPair (since := "2025-05-27")]
def toDualRight : N ≃ₗ[R] Dual R M :=
  toDualLeft p.flip

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