Theorem: Polynomial.discConv_sum (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
s : Finset ι
P : ι → R[X]
⊢ discConv w (∑ i ∈ s, P i) = ∑ i ∈ s, discConv w (P i)
Tactic:
simp [discConv, smul_sum, Finsupp.sum]
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✝ : R[X]
w : R →₀ S
s : Finset ι
P : ι → R[X]
⊢ ∑ x ∈ w.support, ∑ x_1 ∈ s, w x • (P x_1).comp (X + C x) = ∑ x ∈ s, ∑ x_1 ∈ w.support, w x_1 • (P x).comp (X + C x_1)

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
s : Finset ι
P : ι → R[X]
⊢ ∑ x ∈ w.support, ∑ x_1 ∈ s, w x • (P x_1).comp (X + C x) = ∑ x ∈ s, ∑ x_1 ∈ w.support, w x_1 • (P x).comp (X + C x_1)
Tactic:
exact Finset.sum_comm
State after:
no goals