Theorem: MvPowerSeries.monomial_eq' (DividedPowers/ForMathlib/MvPowerSeries/Substitutions.lean)

State before:
σ : Type u_1
inst✝¹ : DecidableEq σ
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : σ → R
⊢ (monomial R e) (e.prod fun s n => r s ^ n) = e.prod fun s e => (r s • X s) ^ e
Tactic:
rw [prod_smul_X_eq_smul_monomial_one, ← map_smul, smul_eq_mul, mul_one]
State after:
no goals