addCommMonoid — Mathlib

English

For a finite index set α, sum of a family of continuous multilinear maps evaluated at m equals the sum of evaluations: (s.sum f a) m = sum (a∈s) f(a) m.

Русский

Сумма по индексу α даёт сумму значений на m.

LaTeX

$$$\\big(\\sum_{a\\in \\alpha} f(a)\\big)(m) = \\sum_{a\\in \\alpha} f(a)(m).$$$

Lean4

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

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