∀ {R : Type u_2} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S} [IsDomain S]
  [inst_4 : DecidableEq S] {y : S},
  (Polynomial.aeval y) (minpoly R x) = 0 →
    Polynomial.eval y (minpolyDiv R x) = if x = y then (Polynomial.aeval x) (Polynomial.derivative (minpoly R x)) else 0