English
Evaluating a polynomial given by a finsupp representation equals the corresponding lift of the finsupp via liftNC along powersHom.
Русский
Оценка полинома, заданного представлением в виде finsupp, равна соответствующему отображению liftNC через powersHom.
LaTeX
$$$\operatorname{ev}_{f,x}\bigl\{\!\text{toFinsupp} := p\} = \operatorname{liftNC}(\uparrow f)\bigl(\text{powersHom } S\ x\bigr) p$$$
Lean4
theorem eval₂_sum (p : T[X]) (g : ℕ → T → R[X]) (x : S) : (p.sum g).eval₂ f x = p.sum fun n a => (g n a).eval₂ f x :=
by
let T : R[X] →+ S :=
{ toFun := eval₂ f x
map_zero' := eval₂_zero _ _
map_add' := fun p q => eval₂_add _ _ }
have A : ∀ y, eval₂ f x y = T y := fun y => rfl
simp only [A]
rw [sum, map_sum, sum]
