Theorem: PolynomialMap.IsHomogeneousOfDegree_smul (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 : ℕ
r : R
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree p f
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
s : S
m : S ⊗[R] M
⊢ (r • f).toFun' S (s • m) = s ^ p • (r • f).toFun' S m
Tactic:
simp only [smul_def, Pi.smul_apply, hf S]
State after:
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 : ℕ
r : R
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree p f
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
s : S
m : S ⊗[R] M
⊢ r • s ^ p • f.toFun' S m = s ^ p • r • f.toFun' S m

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 : ℕ
r : R
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree p f
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
s : S
m : S ⊗[R] M
⊢ r • s ^ p • f.toFun' S m = s ^ p • r • f.toFun' S m
Tactic:
exact smul_comm r (s ^ p) (toFun' f S m)
State after:
no goals