Theorem: MvPolynomial.baseChange_monomial (DividedPowers/DPAlgebra/BaseChange.lean)

State before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
m : σ →₀ ℕ
a : S
⊢ (baseChange φ) ((monomial m) a) = (monomial m) (φ a)
Tactic:
simp only [baseChange, coe_mk, coe_eval₂RingHom, eval₂_monomial, RingHom.coe_comp,
  RingHom.coe_coe, Function.comp_apply]
State after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
m : σ →₀ ℕ
a : S
⊢ (C (φ a) * m.prod fun n e => X n ^ e) = (monomial m) (φ a)

State before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
m : σ →₀ ℕ
a : S
⊢ (C (φ a) * m.prod fun n e => X n ^ e) = (monomial m) (φ a)
Tactic:
rw [monomial_eq]
State after:
no goals