toDualLeft

Mathlib.LinearAlgebra.PerfectPairing.Basic

URI: https://scilib.ai/kg/mathlib#PerfectPairing.toDualLeft

← MathLib Explorer

English

For any a ∈ M, p.toDualLeft a equals the bilinear map p(a).

Русский

Для любого a ∈ M, отображение p.toDualLeft a равно форме p(a).

LaTeX

$$$p.toDualLeft a = p a$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru