no goals
M : Type ?u.101578
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
g' : G ⧸ stabilizer G x
⊢ g • (X - ↑C (ofQuotientStabilizer G x g')) = X - ↑C (ofQuotientStabilizer G x ((fun x_1 x_2 => x_1 • x_2) g g'))
rw [ofQuotientStabilizer_smul, smul_sub, Polynomial.smul_X, Polynomial.smul_C]