R : Type u
S : Type v
a✝ b c d : R
n m✝ : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.705453
a : R
p : R[X]
m : ℕ
hm : degree p < ↑m
⊢ coeff (a • p) m = 0
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.705453
a : R
p : R[X]
⊢ degree (a • p) ≤ degree p
refine (degree_le_iff_coeff_zero _ _).2 fun m hm => ?_
R : Type u
S : Type v
a✝ b c d : R
n m✝ : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.705453
a : R
p : R[X]
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → coeff p m_1 = 0
⊢ coeff (a • p) m = 0
R : Type u
S : Type v
a✝ b c d : R
n m✝ : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.705453
a : R
p : R[X]
m : ℕ
hm : degree p < ↑m
⊢ coeff (a • p) m = 0
rw [degree_lt_iff_coeff_zero] at hm
no goals
R : Type u
S : Type v
a✝ b c d : R
n m✝ : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.705453
a : R
p : R[X]
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → coeff p m_1 = 0
⊢ coeff (a • p) m = 0
simp [hm m le_rfl]