English
The embedding respects the underlying function: the coe of the composition equals the composition of the coes.
Русский
Встраивание сохраняет отображение функций: образец композиции чередующегося отображения равен композиции его естественных кофункций.
LaTeX
$$$ \big(g\circ_{\mathrm{Alt}} f\big)(v) = g\big(f(v)\big)$$$
Lean4
/-- The natural equivalence between linear maps from `M` to `N`
and `1`-multilinear alternating maps from `M` to `N`. -/
@[simps!]
def ofSubsingleton [Subsingleton ι] (i : ι) : (M →ₗ[R] N) ≃ (M [⋀^ι]→ₗ[R] N)
where
toFun f := ⟨MultilinearMap.ofSubsingleton R M N i f, fun _ _ _ _ ↦ absurd (Subsingleton.elim _ _)⟩
invFun f := (MultilinearMap.ofSubsingleton R M N i).symm f
right_inv _ := coe_multilinearMap_injective <| (MultilinearMap.ofSubsingleton R M N i).apply_symm_apply _
