Theorem: Polynomial.discConv_sub_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]
v w : R →₀ S
P : R[X]
⊢ ∀ (a : R) (b₁ b₂ : S), (b₁ - b₂) • P.comp (X + C a) = b₁ • P.comp (X + C a) - b₂ • P.comp (X + C a)
Tactic:
simp [sub_smul]
State after:
no goals