-rw-r--r-- 159 leangoppa-20230726/Goppadecoding/diff.lean raw
import Mathlib.RingTheory.Polynomial.Basic

namespace Polynomial

variable {R: Type _} [Semiring R]

noncomputable def diff: R[X] → R[X] := derivative.toFun