Theorem: Polynomial.eval_discConv (LeanCamCombi/DiscreteDeriv.lean)

State before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
w : R →₀ S
P : R[X]
x : R
⊢ eval x (discConv w P) = w.sum fun r s => s • eval (x + r) P
Tactic:
simp [discConv, Finsupp.sum,eval_finset_sum]
State after:
no goals