Theorem: MvPolynomial.eval₂Hom.smul (DividedPowers/DPAlgebra/Misc.lean)

State before:
R : Type u_2
S : Type u_1
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
r : R
P : MvPolynomial σ R
⊢ (eval₂Hom f g) (r • P) = f r • (eval₂Hom f g) P
Tactic:
simp only [smul_eq_C_mul, coe_eval₂Hom, eval₂_mul, eval₂_C, Algebra.id.smul_eq_mul]
State after:
no goals