R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.655
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ (Finset.sup (support p) fun s => ↑toMultiset s) = Finset.sup (support p) fun s => ↑toMultiset s
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.655
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ degrees p = Finset.sup (support p) fun s => ↑toMultiset s
rw [degrees]
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.655
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ (Finset.sup (support p) fun s => ↑toMultiset s) = Finset.sup (support p) fun s => ↑toMultiset s
convert rfl