simp [discConv]
ι : 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]
r : R
s : S
⊢ discConv (fun₀ | r => s) P = s • P.comp (X + C r)
no goals