addCommMonoid — Mathlib

English

The sum of multilinear maps evaluated at m equals the sum of their evaluations: (∑ a∈s f(a))(m) = ∑ a∈s f(a)(m).

Русский

Сумма мультилейных отображений, применённых к m, равна сумме их значений: (∑ a∈s f(a))(m) = ∑ a∈s f(a)(m).

LaTeX

$$$\forall m, \left(\sum_{a\in s} f(a)\right)(m) = \sum_{a\in s} f(a)(m)$$$

Lean4

instance addCommMonoid : AddCommMonoid (MultilinearMap R M₁ M₂) :=
  coe_injective.addCommMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl

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