Theorem: Polynomial.baseChange_monomial (DividedPowers/PolynomialMap/Homogeneous.lean)

State before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_3
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
n : ℕ
a : S
⊢ (baseChange φ) ((monomial n) a) = (monomial n) (φ a)
Tactic:
simp only [baseChange, AlgHom.coe_mk, coe_eval₂RingHom, eval₂_monomial, RingHom.coe_comp,
  RingHom.coe_coe, Function.comp_apply, C_mul_X_pow_eq_monomial]
State after:
no goals