Theorem: PolynomialMap.isHomogeneousOfDegree_ground (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 : M →ₚ[R] N
hf : IsHomogeneousOfDegree p f
r : R
m : M
⊢ f.ground (r • m) = r ^ p • f.ground m
Tactic:
simp only [ground, Function.comp_apply, map_smul, TensorProduct.lid_symm_apply, hf R r]
State after:
no goals