English
The exterior power dual can be identified with the dual of the exterior power via the pairingDual map.
Русский
Через отображение pairingDual можно идентифицировать двойственное пространство ∧^n(M^*) с двойственным пространством ∧^n M.
LaTeX
$$$ pairingDual(R\, M\, n) : ⋀[R]^n (Module.Dual R M) \rightarrowₗ[R] Module.Dual R (⋀[R]^n M) $$$
Lean4
/-- The linear map from the exterior power of the dual to the dual of the exterior power. -/
noncomputable def pairingDual (n : ℕ) : ⋀[R]^n (Module.Dual R M) →ₗ[R] Module.Dual R (⋀[R]^n M) :=
alternatingMapLinearEquiv (alternatingMapToDual R M n)