R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : R[X]
qn : natDegree q ≤ n
h : natDegree (p + q) ≤ n
⊢ natDegree p ≤ n
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : R[X]
qn : natDegree q ≤ n
⊢ natDegree (p + q) ≤ n ↔ natDegree p ≤ n
refine' ⟨fun h => _, fun h => natDegree_add_le_of_degree_le h qn⟩
R : Type u
S : Type v
ι : Type w
a b : R
m✝ n✝ : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : R[X]
qn : natDegree q ≤ n
h : natDegree (p + q) ≤ n
m : ℕ
hm : n < m
⊢ coeff p m = 0
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : R[X]
qn : natDegree q ≤ n
h : natDegree (p + q) ≤ n
⊢ natDegree p ≤ n
refine' natDegree_le_iff_coeff_eq_zero.mpr fun m hm => _
case h.e'_2
R : Type u
S : Type v
ι : Type w
a b : R
m✝ n✝ : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : R[X]
qn : natDegree q ≤ n
h : natDegree (p + q) ≤ n
m : ℕ
hm : n < m
⊢ coeff p m = coeff (p + q) m
R : Type u
S : Type v
ι : Type w
a b : R
m✝ n✝ : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : R[X]
qn : natDegree q ≤ n
h : natDegree (p + q) ≤ n
m : ℕ
hm : n < m
⊢ coeff p m = 0
convert natDegree_le_iff_coeff_eq_zero.mp h m hm using 1
no goals
case h.e'_2
R : Type u
S : Type v
ι : Type w
a b : R
m✝ n✝ : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : R[X]
qn : natDegree q ≤ n
h : natDegree (p + q) ≤ n
m : ℕ
hm : n < m
⊢ coeff p m = coeff (p + q) m
rw [coeff_add, natDegree_le_iff_coeff_eq_zero.mp qn _ hm, add_zero]