R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.41650
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
⊢ 0 ≤ 0 • degrees p
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.41650
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
⊢ degrees (p ^ 0) ≤ 0 • degrees p
rw [pow_zero, degrees_one]
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.41650
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
⊢ 0 ≤ 0 • degrees p
exact Multiset.zero_le _
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.41650
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
n : ℕ
⊢ degrees (p * p ^ n) ≤ degrees p + n • degrees p
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.41650
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
n : ℕ
⊢ degrees (p ^ (n + 1)) ≤ (n + 1) • degrees p
rw [pow_succ, add_smul, add_comm, one_smul]
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.41650
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
n : ℕ
⊢ degrees (p * p ^ n) ≤ degrees p + n • degrees p
exact le_trans (degrees_mul _ _) (add_le_add_left (degrees_pow _ n) _)