∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : CommRing S] {p : Polynomial S}
  [inst_3 : Algebra S R],
  Function.Injective ⇑(algebraMap S R) → ∀ {x : R}, p ≠ 0 → (x ∈ p.rootSet R ↔ (Polynomial.aeval x) p = 0)