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

State before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
e : σ →₀ ℕ
r : R
⊢ (substAlgHom ha) ((monomial R e) r) = (algebraMap R (MvPowerSeries τ S)) r * e.prod fun s n => a s ^ n
Tactic:
rw [← MvPolynomial.coe_monomial, substAlgHom_coe, MvPolynomial.aeval_monomial]
State after:
no goals