Theorem: PolynomialMap.IsHomogeneousOfDegree_add (DividedPowers/PolynomialMap/Homogeneous.lean)

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ℕ
f g : M →ₚ[R] N
hf : IsHomogeneousOfDegree p f
hg : IsHomogeneousOfDegree p g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
s : S
m : S ⊗[R] M
⊢ (f + g).toFun' S (s • m) = s ^ p • (f + g).toFun' S m
Tactic:
simp only [add_def_apply, smul_add, hf S s m, hg S s m]
State after:
no goals