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

State before:
σ : Type u_2
τ : Type ?u.26920
R : Type u_1
inst✝ : CommSemiring R
S : Type ?u.26929
p : MvPolynomial σ R
⊢ p.totalDegree = 0 ↔ ∀ m ∈ p.support, ∀ (x : σ), m x = 0
Tactic:
rw [totalDegree_eq_weightedTotalDegree, weightedTotalDegree_eq_zero_iff _ p]
State after:
σ : Type u_2
τ : Type ?u.26920
R : Type u_1
inst✝ : CommSemiring R
S : Type ?u.26929
p : MvPolynomial σ R
⊢ NonTorsionWeight 1

State before:
σ : Type u_2
τ : Type ?u.26920
R : Type u_1
inst✝ : CommSemiring R
S : Type ?u.26929
p : MvPolynomial σ R
⊢ NonTorsionWeight 1
Tactic:
exact unit_weight_is_nonTrivialWeight
State after:
no goals