coe_multilinearMap_mk — Mathlib

English

Extending an alternating map from a multilinear map preserves the embedding into the multilinear representation.

Русский

Расширение чередующегося отображения из много-линейного отображения сохраняет вложение в много-линейное представление.

LaTeX

$$Eq { toFun := f, map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := h }.toMultilinearMap$$

Lean4

theorem coe_multilinearMap_mk (f : (ι → M) → N) (h₁ h₂ h₃) :
    ((⟨⟨f, h₁, h₂⟩, h₃⟩ : M [⋀^ι]→ₗ[R] N) : MultilinearMap R (fun _ : ι => M) N) = ⟨f, @h₁, @h₂⟩ := by simp

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