Theorem: MvPowerSeries.monomial_one_eq (DividedPowers/ForMathlib/MvPowerSeries/Substitutions.lean)

State before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
⊢ (monomial R e) 1 = e.prod fun s n => X s ^ n
Tactic:
simp only [← MvPolynomial.coe_X, ← MvPolynomial.coe_pow, ← MvPolynomial.coe_monomial, MvPolynomial.monomial_eq, map_one, one_mul]
State after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
⊢ ↑(e.prod fun n e => MvPolynomial.X n ^ e) = e.prod fun s n => ↑(MvPolynomial.X s ^ n)

State before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
⊢ ↑(e.prod fun n e => MvPolynomial.X n ^ e) = e.prod fun s n => ↑(MvPolynomial.X s ^ n)
Tactic:
simp only [← MvPolynomial.coeToMvPowerSeries.ringHom_apply, ← map_finsupp_prod]
State after:
no goals