English
The additive structure on multilinear maps is compatible with the underlying set-theoretic addition; basic properties follow from the pointwise definition.
Русский
Аддитивная структура мультилейных отображений совместима с встроенным сложением; базовые свойства следуют из определения по точке.
LaTeX
$$$\text{Add} \;\text{structure}$ is compatible with pointwise addition$$
Lean4
/-- Combine a family of multilinear maps with the same domain and codomains `M' i` into a
multilinear map taking values in the space of functions `∀ i, M' i`. -/
@[simps]
def pi {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)] [∀ i, Module R (M' i)]
(f : ∀ i, MultilinearMap R M₁ (M' i)) : MultilinearMap R M₁ (∀ i, M' i)
where
toFun m i := f i m
map_update_add' _ _ _ _ := funext fun j => (f j).map_update_add _ _ _ _
map_update_smul' _ _ _ _ := funext fun j => (f j).map_update_smul _ _ _ _
