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

State before:
σ : Type u_1
τ : Type ?u.203
R : Type ?u.206
inst✝ : CommSemiring R
S : Type ?u.212
d : σ →₀ ℕ
⊢ degree d = ∑ i ∈ d.support, d i
Tactic:
simp [degree, weightedDegree, Finsupp.total, Finsupp.sum]
State after:
no goals