R : Type u
S : Type v
T : Type w
A : Type z
a✝ b✝ : R
n : ℕ
inst✝ : CommRing R
p✝ q : R[X]
a b : R
p : R[X]
⊢ X - ↑C b ∣ p - ↑C (eval b p)
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b✝ : R
n : ℕ
inst✝ : CommRing R
p✝ q : R[X]
a b : R
p : R[X]
⊢ a - b ∣ eval a p - eval b p
suffices X - C b ∣ p - C (p.eval b) by
  simpa only [coe_evalRingHom, eval_sub, eval_X, eval_C] using (evalRingHom a).map_dvd this
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]
a b : R
p : R[X]
⊢ X - ↑C b ∣ p - ↑C (eval b p)
simp [dvd_iff_isRoot]
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]
a b : R
p : R[X]
this : X - ↑C b ∣ p - ↑C (eval b p)
⊢ a - b ∣ eval a p - eval b p
simpa only [coe_evalRingHom, eval_sub, eval_X, eval_C] using (evalRingHom a).map_dvd this