eval₂_multiset_sum — Mathlib

English

Evaluation respects the sum over a multiset: evaluating the multiset sum equals the sum of evaluations of each element.

Русский

Оценка сохраняет сумму над мультимножестом: сумма по мультимножесту равна сумме оценок элементов.

LaTeX

$$$\operatorname{ev}_{f,x}(s.sum) = (s.map (\operatorname{ev}_{f,x})).sum$$

Lean4

theorem eval₂_multiset_sum (s : Multiset R[X]) (x : S) : eval₂ f x s.sum = (s.map (eval₂ f x)).sum :=
  map_multiset_sum (eval₂AddMonoidHom f x) s

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