eval_multisetSum — Mathlib

English

Polynomial evaluation commutes with Multiset.sum: eval x s.sum = (s.map (eval x)).sum.

Русский

Оценивание полиномов коммутирует с суммой мультисета: eval x s.sum = (s.map (eval x)).sum.

LaTeX

$$$ \mathrm{eval}\ x \ s.\mathrm{sum} = (s.\mathrm{map}(\mathrm{eval}\ x)).\mathrm{sum} $$$

Lean4

/-- Polynomial evaluation commutes with `Multiset.sum`. -/
theorem eval_multisetSum (s : Multiset R[X]) (x : R) : eval x s.sum = (s.map (eval x)).sum :=
  eval₂_multiset_sum ..

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