coeAddMonoidHom — Mathlib

English

Sum of multilinear maps is multilinear and its value at m equals the sum of the values at m.

Русский

Сумма мультилнейных отображений является мультилейной и равна сумме их значений на входе.

LaTeX

$$$\forall f,g: MultilinearMap R M_1 M_2, \forall m, (f+g)(m) = f(m) + g(m)$$$

Lean4

/-- Coercion of a multilinear map to a function as an additive monoid homomorphism. -/
@[simps]
def coeAddMonoidHom : MultilinearMap R M₁ M₂ →+ (((i : ι) → M₁ i) → M₂) where toFun := DFunLike.coe; map_zero' := rfl;
  map_add' _ _ := rfl

Похожие утверждения