English
The toAlternatingMap operator is additive on continuous alternating maps: (f+g).toAlternatingMap = f.toAlternatingMap + g.toAlternatingMap.
Русский
Оператор toAlternatingMap сохраняет сложение: (f+g).toAlternatingMap = f.toAlternatingMap + g.toAlternatingMap.
LaTeX
$$$ (f + g).toAlternatingMap = f.toAlternatingMap + g.toAlternatingMap $$$
Lean4
/-- The natural equivalence between continuous linear maps from `M` to `N`
and continuous 1-multilinear alternating maps from `M` to `N`. -/
@[simps! apply_apply symm_apply_apply apply_toContinuousMultilinearMap]
def ofSubsingleton [Subsingleton ι] (i : ι) : (M →L[R] N) ≃ M [⋀^ι]→L[R] N
where
toFun
f :=
{ AlternatingMap.ofSubsingleton R M N i f with
toContinuousMultilinearMap := ContinuousMultilinearMap.ofSubsingleton R M N i f }
invFun f := (ContinuousMultilinearMap.ofSubsingleton R M N i).symm f.1
right_inv
_ := toContinuousMultilinearMap_injective <| (ContinuousMultilinearMap.ofSubsingleton R M N i).apply_symm_apply _
