no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
h : divX p = 0
⊢ p = ↑C (coeff p 0)
simpa [eq_comm, h] using divX_mul_X_add p
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
h : p = ↑C (coeff p 0)
⊢ divX p = 0
rw [h, divX_C]