∀ {T : Type w} [inst : CommRing T] {p : Polynomial T} {S : Type u_1} [IsDomain T] [inst_2 : CommRing S]
  [inst_3 : IsDomain S] [inst_4 : Algebra T S] [Module.IsTorsionFree T S] {a : S},
  a ∈ p.rootSet S ↔ p ≠ 0 ∧ (Polynomial.aeval a) p = 0