coe_mk — Mathlib

English

Constructing an alternating map from a multilinear map and witnesses of alternation yields an alternating map whose evaluation agrees with the original multilinear map.

Русский

Построение чередующегося отображения из многочленного линейного отображения с доказательствами чередности даёт такое же отображение при оценке.

LaTeX

$$$((⟨⟨f, h_1, h_2⟩, h_3⟩ : M [⋀^ι]→ₗ[R] N) : MultilinearMap R (fun _ : ι => M) N) = ⟨f, @h_1, @h_2⟩$$$

Lean4

@[simp]
theorem coe_mk (f : MultilinearMap R (fun _ : ι => M) N) (h) : ⇑(⟨f, h⟩ : M [⋀^ι]→ₗ[R] N) = f :=
  rfl

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