toLinearMap_apply — Mathlib

English

The map p.toDualLeft is a linear equivalence M ≃ Dual_R N induced by a perfect pairing.

Русский

Пусть имеется совершенная пара; тогда отображение p.toDualLeft задаёт линейное эквивалентное отображение M ≃ Dual_R N.

LaTeX

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

Lean4

@[deprecated "No replacement" (since := "2025-05-27")]
theorem toLinearMap_apply (p : PerfectPairing R M N) (x : M) : p.toLinearMap x = p x :=
  rfl

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