English
piFamilyₗ realizes the correspondence between a family of multilinear maps and a single multilinear map over the product space with coordinates, preserving linear structure.
Русский
piFamilyₗ реализует соответствие между семейством мультиленейных отображений и одним мультиленейным отображением над произведением пространств координат, сохраняя линейную структуру.
LaTeX
$$$\piFamily_{\ell}: (f) \mapsto \text{linear transport of } f$$$
Lean4
/-- `MultilinearMap.piFamily` as a linear map. -/
@[simps]
def piFamilyₗ :
(Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) (N p)) →ₗ[R]
MultilinearMap R (fun i => Π j : κ i, M i j) (Π t : Π i, κ i, N t)
where
toFun := piFamily
map_add' := piFamily_add
map_smul' := piFamily_smul
