R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.598995
p : R[X]
⊢ degree 1 ≤ 0
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.598995
p : R[X]
⊢ degree (p ^ 0) ≤ 0 • degree p
rw [pow_zero, zero_nsmul]
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.598995
p : R[X]
⊢ degree 1 ≤ 0
exact degree_one_le
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.598995
p : R[X]
n : ℕ
⊢ degree (p * p ^ n) ≤ degree p + degree (p ^ n)
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.598995
p : R[X]
n : ℕ
⊢ degree (p ^ (n + 1)) ≤ degree p + degree (p ^ n)
rw [pow_succ]
no goals
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.598995
p : R[X]
n : ℕ
⊢ degree (p * p ^ n) ≤ degree p + degree (p ^ n)
exact degree_mul_le _ _
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.598995
p : R[X]
n : ℕ
⊢ degree p + degree (p ^ n) ≤ degree p + n • degree p
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.598995
p : R[X]
n : ℕ
⊢ degree p + degree (p ^ n) ≤ (n + 1) • degree p
rw [succ_nsmul]
no goals
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.598995
p : R[X]
n : ℕ
⊢ degree p + degree (p ^ n) ≤ degree p + n • degree p
exact add_le_add le_rfl (degree_pow_le _ _)