no goals
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
a x : R
⊢ x ∈ roots (p - ↑C a) ↔ p ≠ ↑C a ∧ eval x p = a
rw [mem_roots', IsRoot.def, sub_ne_zero, eval_sub, sub_eq_zero, eval_C]