R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.469070
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ 0 ≤ List.sum (List.map totalDegree [])
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.469070
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ totalDegree (List.prod []) ≤ List.sum (List.map totalDegree [])
rw [@List.prod_nil (MvPolynomial σ R) _, totalDegree_one]
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.469070
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ 0 ≤ List.sum (List.map totalDegree [])
rfl
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.469070
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
ps : List (MvPolynomial σ R)
⊢ totalDegree (p * List.prod ps) ≤ totalDegree p + List.sum (List.map totalDegree ps)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.469070
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
ps : List (MvPolynomial σ R)
⊢ totalDegree (List.prod (p :: ps)) ≤ List.sum (List.map totalDegree (p :: ps))
rw [@List.prod_cons (MvPolynomial σ R) _, List.map, List.sum_cons]
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.469070
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
ps : List (MvPolynomial σ R)
⊢ totalDegree (p * List.prod ps) ≤ totalDegree p + List.sum (List.map totalDegree ps)
exact le_trans (totalDegree_mul _ _) (add_le_add_left (totalDegree_list_prod ps) _)