Theorem: Polynomial.discConv_zero_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✝ P : R[X]
⊢ discConv 0 P = 0
Tactic:
simp [discConv]
State after:
no goals