∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : IsDomain A] [inst_3 : IsDomain B]
  {p : Polynomial A} {f : A →+* B}, Polynomial.map f p ≠ 0 → p.roots.card ≤ (Polynomial.map f p).roots.card