import Mathlib.RingTheory.Polynomial.Basic namespace Polynomial variable {R: Type _} [Semiring R] noncomputable def diff: R[X] → R[X] := derivative.toFun