Theorem: Polynomial.discConv_sum_weight (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]
s : Finset ι
w : ι → R →₀ S
P : R[X]
⊢ ∀ (i : R), 0 • P.comp (X + C i) = 0
Tactic:
simp
State after:
no goals

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]
s : Finset ι
w : ι → R →₀ S
P : R[X]
⊢ ∀ (i : R) (x y : S), (x + y) • P.comp (X + C i) = x • P.comp (X + C i) + y • P.comp (X + C i)
Tactic:
simp [add_smul]
State after:
no goals