no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.285420
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
⊢ degreeOf n 0 = 0
classical simp only [degreeOf_def, degrees_zero, Multiset.count_zero]
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.285420
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
⊢ degreeOf n 0 = 0
simp only [degreeOf_def, degrees_zero, Multiset.count_zero]