R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.471246
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Multiset (MvPolynomial σ R)
l : List (MvPolynomial σ R)
⊢ totalDegree (Multiset.prod (Quotient.mk (List.isSetoid (MvPolynomial σ R)) l)) ≤
    Multiset.sum (Multiset.map totalDegree (Quotient.mk (List.isSetoid (MvPolynomial σ R)) l))
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.471246
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Multiset (MvPolynomial σ R)
⊢ totalDegree (Multiset.prod s) ≤ Multiset.sum (Multiset.map totalDegree s)
refine' Quotient.inductionOn s fun l => _
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.471246
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Multiset (MvPolynomial σ R)
l : List (MvPolynomial σ R)
⊢ totalDegree (List.prod l) ≤ List.sum (List.map totalDegree l)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.471246
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Multiset (MvPolynomial σ R)
l : List (MvPolynomial σ R)
⊢ totalDegree (Multiset.prod (Quotient.mk (List.isSetoid (MvPolynomial σ R)) l)) ≤
    Multiset.sum (Multiset.map totalDegree (Quotient.mk (List.isSetoid (MvPolynomial σ R)) l))
rw [Multiset.quot_mk_to_coe, Multiset.coe_prod, Multiset.coe_map, Multiset.coe_sum]
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.471246
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Multiset (MvPolynomial σ R)
l : List (MvPolynomial σ R)
⊢ totalDegree (List.prod l) ≤ List.sum (List.map totalDegree l)
exact totalDegree_list_prod l