Theorem: MvPolynomial.isHomogeneous_of_totalDegree_zero_iff (DividedPowers/ForMathlib/Homogeneous.lean)

State before:
σ : Type u_2
τ : Type ?u.27316
R : Type u_1
inst✝ : CommSemiring R
S : Type ?u.27325
p : MvPolynomial σ R
⊢ p.totalDegree = 0 ↔ p.IsHomogeneous 0
Tactic:
rw [totalDegree_eq_weightedTotalDegree,
  ← isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero, IsHomogeneous]
State after:
no goals