no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.460088
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
c : R
hc : c ≠ 0
⊢ totalDegree (↑(monomial s) c) = sum s fun x e => e
classical simp [totalDegree, support_monomial, if_neg hc]
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.460088
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
c : R
hc : c ≠ 0
⊢ totalDegree (↑(monomial s) c) = sum s fun x e => e
simp [totalDegree, support_monomial, if_neg hc]