∀ {R : Type u} [inst : CommRing R] [NoZeroDivisors R] [CharZero R] {p : Polynomial R} {t : R},
  p.IsRoot t → Polynomial.rootMultiplicity t (Polynomial.derivative p) = Polynomial.rootMultiplicity t p - 1