R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.326493
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
⊢ (Finset.sup (support p) fun s => sum s fun x e => e) = Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.326493
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
⊢ totalDegree p = Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)
rw [totalDegree]
case e_f
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.326493
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
⊢ (fun s => sum s fun x e => e) = fun m => ↑Multiset.card (↑toMultiset m)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.326493
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
⊢ (Finset.sup (support p) fun s => sum s fun x e => e) = Finset.sup (support p) fun m => ↑Multiset.card (↑toMultiset m)
congr
case e_f.h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.326493
r : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ (sum m fun x e => e) = ↑Multiset.card (↑toMultiset m)
case e_f
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.326493
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
⊢ (fun s => sum s fun x e => e) = fun m => ↑Multiset.card (↑toMultiset m)
funext m
no goals
case e_f.h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.326493
r : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ (sum m fun x e => e) = ↑Multiset.card (↑toMultiset m)
exact (Finsupp.card_toMultiset _).symm