Theorem: PolynomialMap.mem_grade (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
f : M →ₚ[R] N
p : ℕ
⊢ f ∈ grade p ↔ IsHomogeneousOfDegree p f
Tactic:
rfl
State after:
no goals