multilinearMapToDual_apply_tprod — Mathlib

English

There is a linear map that pairs the tensor power of the dual with the tensor power itself to produce an element of the dual of the tensor power, built via lifting a multilinear map to the dual level.

Русский

Существует линейное отображение, сопрягающее тензорную степень двойственного пространства с тензорной степенью сами по себе, дающее элемент двойственного пространства тензорного произведения, построенное через поднесение мультилинейной карты на уровень двойственности.

LaTeX

$$$ \\text{pairingDual}: ⨂[R]^n (M^*) \\to (⨂[R]^n M)^* $$$

Lean4

@[simp]
theorem multilinearMapToDual_apply_tprod (f : (_ : Fin n) → Module.Dual R M) (v : Fin n → M) :
    multilinearMapToDual R M n f (tprod _ v) = ∏ i, (f i (v i)) := by simp [multilinearMapToDual]

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