eval₂_list_sum — Mathlib

English

A variant form of evaluating a finsupp-represented polynomial equals liftNC applied to p.

Русский

Вариант формы оценки полинома, заданного finsupp, равен liftNC применённому к p.

LaTeX

$$$\operatorname{ev}_{f,x}\bigl\{\!\text{toFinsupp} := p\} = \operatorname{liftNC}(\uparrow f)(\text{powersHom } S\ x) p$$$

Lean4

theorem eval₂_list_sum (l : List R[X]) (x : S) : eval₂ f x l.sum = (l.map (eval₂ f x)).sum :=
  map_list_sum (eval₂AddMonoidHom f x) l

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