simp only [scaleRoots_C, derivative_C, zero_scaleRoots]
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p = C (p.coeff 0)
⊢ derivative ((C (p.coeff 0)).scaleRoots r) = (derivative (C (p.coeff 0))).scaleRoots r
no goals