∀ {R : Type u_1} {K : Type u_4} [inst : CommSemiring R] [inst_1 : Field K] [inst_2 : Algebra R K],
  Function.Injective ⇑(algebraMap R K) →
    ∀ {p : Polynomial R} {r s : R},
      (Polynomial.aeval ((algebraMap R K) r / (algebraMap R K) s)) p = 0 →
        s ∈ nonZeroDivisors R → (Polynomial.aeval ((algebraMap R K) r)) (p.scaleRoots s) = 0