R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.515454
H : p ≠ 0
⊢ coeff p (natDegree p) ≠ 0
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.515454
H : p ≠ 0
⊢ natDegree p ∈ support p
rw [mem_support_iff]
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.515454
H : p ≠ 0
⊢ coeff p (natDegree p) ≠ 0
exact (not_congr leadingCoeff_eq_zero).mpr H