no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.350050
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
⊢ totalDegree p ≤ ↑Multiset.card (degrees p)
classical
rw [totalDegree_eq]
exact Finset.sup_le fun s hs => Multiset.card_le_of_le <| Finset.le_sup hs
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.350050
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
⊢ (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) ≤ ↑Multiset.card (degrees p)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.350050
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
⊢ totalDegree p ≤ ↑Multiset.card (degrees p)
rw [totalDegree_eq]
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.350050
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
⊢ (Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)) ≤ ↑Multiset.card (degrees p)
exact Finset.sup_le fun s hs => Multiset.card_le_of_le <| Finset.le_sup hs