no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.5165
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ degrees (↑(monomial s) a) = ↑toMultiset s
classical
  refine' le_antisymm (degrees_monomial s a) <| Finset.le_sup <| _
  rw [support_monomial, if_neg ha, Finset.mem_singleton]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.5165
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ s ∈ support (↑(monomial s) a)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.5165
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ degrees (↑(monomial s) a) = ↑toMultiset s
refine' le_antisymm (degrees_monomial s a) <| Finset.le_sup <| _
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.5165
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ s ∈ support (↑(monomial s) a)
rw [support_monomial, if_neg ha, Finset.mem_singleton]