∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {t : R},
  Polynomial.eval t ((⇑Polynomial.derivative)^[Polynomial.rootMultiplicity t p] p) =
    (Polynomial.rootMultiplicity t p).factorial •
      Polynomial.eval t (p /ₘ (Polynomial.X - Polynomial.C t) ^ Polynomial.rootMultiplicity t p)