Theorem: Polynomial.eval_discBackwardDiff (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✝ P : R[X]
x : R
⊢ eval x P.discBackwardDiff = eval x P - eval (x - 1) P
Tactic:
simp_rw [discBackwardDiff, discConv_sub_weight, discConv_single]
State after:
ι : 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✝ P : R[X]
x : R
⊢ eval x (1 • P.comp (X + C 0) - 1 • P.comp (X + C (-1))) = eval x P - eval (x - 1) P

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✝ P : R[X]
x : R
⊢ eval x (1 • P.comp (X + C 0) - 1 • P.comp (X + C (-1))) = eval x P - eval (x - 1) P
Tactic:
simp [sub_eq_add_neg]
State after:
no goals