R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.472102
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
s : Finset ι
f : ι → MvPolynomial σ R
⊢ Multiset.sum (Multiset.map totalDegree (Multiset.map f s.val)) ≤ ∑ i in s, totalDegree (f i)
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.472102
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
s : Finset ι
f : ι → MvPolynomial σ R
⊢ totalDegree (Finset.prod s f) ≤ ∑ i in s, totalDegree (f i)
refine' le_trans (totalDegree_multiset_prod _) _
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.472102
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
s : Finset ι
f : ι → MvPolynomial σ R
⊢ Multiset.sum (Multiset.map (totalDegree ∘ f) s.val) ≤ ∑ i in s, totalDegree (f i)
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.472102
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
s : Finset ι
f : ι → MvPolynomial σ R
⊢ Multiset.sum (Multiset.map totalDegree (Multiset.map f s.val)) ≤ ∑ i in s, totalDegree (f i)
rw [Multiset.map_map]
no goals
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.472102
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
s : Finset ι
f : ι → MvPolynomial σ R
⊢ Multiset.sum (Multiset.map (totalDegree ∘ f) s.val) ≤ ∑ i in s, totalDegree (f i)
rfl