∀ {A : Type u_1} {K : Type u_2} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A]
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] {p : Polynomial A} {r : K},
  (Polynomial.aeval r) p = 0 → ↑(IsFractionRing.den A r) ∣ p.leadingCoeff