no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q : R[X]
c : R[X]ˣ
p : R[X]
⊢ coeff (↑c) 0 • p = ↑c * p
rw [← Polynomial.C_mul', ← Polynomial.eq_C_of_degree_eq_zero (degree_coe_units c)]