no goals
A : Type ?u.2391
K : Type ?u.2394
R : Type u_1
S : Type ?u.2400
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
i : ℕ
⊢ coeff (scaleRoots p s) i = coeff p i * s ^ (natDegree p - i)
simp (config := { contextual := true }) [scaleRoots, coeff_monomial]