Theorem: MvPowerSeries.monomial_smul_const (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) (r ^ e.sum fun x n => n) = e.prod fun s e => (r • X s) ^ e
Tactic:
rw [prod_smul_X_eq_smul_monomial_one, ← map_smul, smul_eq_mul, mul_one]
State after:
σ : Type u_1
inst✝¹ : DecidableEq σ
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : R
⊢ (monomial R e) (r ^ e.sum fun x n => n) = (monomial R e) (e.prod fun s n => r ^ n)

State before:
σ : Type u_1
inst✝¹ : DecidableEq σ
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : R
⊢ (monomial R e) (r ^ e.sum fun x n => n) = (monomial R e) (e.prod fun s n => r ^ n)
Tactic:
simp only [Finsupp.sum, Finsupp.prod, Finset.prod_pow_eq_pow_sum]
State after:
no goals