no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
f : R[X]
x✝ : X ∣ f
g : R[X]
hfg : f = X * g
⊢ coeff f 0 = 0
rw [hfg, mul_comm, coeff_mul_X_zero]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
f : R[X]
hf : coeff f 0 = 0
⊢ f = X * divX f
rw [mul_comm, ← add_zero (f.divX * X), ← C_0, ← hf, divX_mul_X_add]