no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
r : R
⊢ ↑(expand R p) (↑(monomial q) r) = ↑(monomial (q * p)) r
simp_rw [← smul_X_eq_monomial, AlgHom.map_smul, AlgHom.map_pow, expand_X, mul_comm, pow_mul]