∀ {S : Type u_2} {K : Type u_4} [inst : Semiring S] [inst_1 : Field K] {p : Polynomial S} {f : S →+* K},
  Function.Injective ⇑f →
    ∀ {r s : S},
      Polynomial.eval₂ f (f r / f s) p = 0 → s ∈ nonZeroDivisors S → Polynomial.eval₂ f (f r) (p.scaleRoots s) = 0