no goals
M : Type ?u.109284
inst✝⁴ : Monoid M
G : Type u_2
inst✝³ : Group G
inst✝² : Fintype G
R : Type u_1
inst✝¹ : CommRing R
inst✝ : MulSemiringAction G R
x : R
g : G
n : ℕ
⊢ g • Polynomial.coeff (prodXSubSmul G R x) n = Polynomial.coeff (prodXSubSmul G R x) n
rw [← Polynomial.coeff_smul, prodXSubSmul.smul]