no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
h : X - ↑C a ∣ p
⊢ IsRoot p a
rwa [← dvd_iff_modByMonic_eq_zero (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval, ← C_0,
  C_inj] at h
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p q : R[X]
h : IsRoot p a
⊢ p = (X - ↑C a) * (p /ₘ (X - ↑C a))
rw [mul_divByMonic_eq_iff_isRoot.2 h]