pairingDual — Mathlib

English

The pairingDual map realizes the canonical linear map from the tensor power of duals to the dual of the tensor power via PiTensorProduct lift.

Русский

Пайринг-дюал отображает каноническое линейное отображение из тензорной степени двойственных в двойственное тензорного произведения через подъем PiTensorProduct.

LaTeX

$$$ pairingDual = \\PiTensorProduct.lift (multilinearMapToDual R M n) $$$

Lean4

/-- The linear map from the tensor power of the dual to the dual of the tensor power. -/
noncomputable def pairingDual : ⨂[R]^n (Module.Dual R M) →ₗ[R] (Module.Dual R (⨂[R]^n M)) :=
  PiTensorProduct.lift (multilinearMapToDual R M n)

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