R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h0 : comp p q = 0
⊢ 0 ≤ natDegree p * natDegree q
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h0 : comp p q = 0
⊢ natDegree (comp p q) ≤ natDegree p * natDegree q
rw [h0, natDegree_zero]
no goals
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h0 : comp p q = 0
⊢ 0 ≤ natDegree p * natDegree q
exact Nat.zero_le _
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
h0 : ¬comp p q = 0
n : ℕ
hn : n ∈ support p
⊢ ↑n * ↑(natDegree q) = ↑(n * natDegree q)
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
h0 : ¬comp p q = 0
n : ℕ
hn : n ∈ support p
⊢ ↑(natDegree (↑C (coeff p n))) + n • ↑(natDegree q) = ↑(n * natDegree q)
rw [natDegree_C, Nat.cast_zero, zero_add, nsmul_eq_mul]
no goals
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
h0 : ¬comp p q = 0
n : ℕ
hn : n ∈ support p
⊢ ↑n * ↑(natDegree q) = ↑(n * natDegree q)
simp