English
The map that sends a continuous alternating map f to its associated continuous multilinear map is linear over R. In particular, toContinuousMultilinearMapLinear is an R-linear map.
Русский
Отображение, переводящее непрерывное чередующее отображение f к соответствующей непрерывной мультиляйней карте, является линейным по отношению к R.
LaTeX
$$$$ toContinuousMultilinearMapLinear : (M [⋀^ι]→L[A] N) \\to_R ContinuousMultilinearMap A (ι ↦ M) N $$ и для любых f,g и a: $$ (toContinuousMultilinearMapLinear (a f + b g)) = a\\,(toContinuousMultilinearMapLinear f) + b\\,(toContinuousMultilinearMapLinear g). $$$$
Lean4
/-- Linear map version of the map `toMultilinearMap` associating to a continuous alternating map
the corresponding multilinear map. -/
@[simps]
def toContinuousMultilinearMapLinear : M [⋀^ι]→L[A] N →ₗ[R] ContinuousMultilinearMap A (fun _ : ι => M) N
where
toFun := toContinuousMultilinearMap
map_add' _ _ := rfl
map_smul' _ _ := rfl
