English
The space of multilinear maps forms an additive commutative monoid under the pointwise addition, with the zero map as the identity and the usual commutativity of addition.
Русский
Пространство мультилейных отображений образует аддитивный коммутативный моноид относительно покоординатного сложения: нулевая карта является нейтральным элементом, а сложение коммутативно.
LaTeX
$$$ (\text{MultilinearMap } R M_1 M_2, +, 0) \text{ is an AddCommMonoid}$$$
Lean4
/-- The Cartesian product of two multilinear maps, as a multilinear map. -/
@[simps]
def prod (f : MultilinearMap R M₁ M₂) (g : MultilinearMap R M₁ M₃) : MultilinearMap R M₁ (M₂ × M₃)
where
toFun m := (f m, g m)
map_update_add' m i x y := by simp
map_update_smul' m i c x := by simp
