R : Type u_1
k : Type u_2
α : Type u_3
inst✝² : Ring R
inst✝¹ : LinearOrderedField k
abv : R → k
inst✝ : IsAbsoluteValue abv
p : R[X]
h : 0 < degree p
l : Filter α
z : α → R
hz : Tendsto (abv ∘ z) l atTop
⊢ ↑(RingHom.id R) (leadingCoeff p) ≠ 0
R : Type u_1
k : Type u_2
α : Type u_3
inst✝² : Ring R
inst✝¹ : LinearOrderedField k
abv : R → k
inst✝ : IsAbsoluteValue abv
p : R[X]
h : 0 < degree p
l : Filter α
z : α → R
hz : Tendsto (abv ∘ z) l atTop
⊢ Tendsto (fun x => abv (eval (z x) p)) l atTop
apply tendsto_abv_eval₂_atTop _ _ _ h _ hz
no goals
R : Type u_1
k : Type u_2
α : Type u_3
inst✝² : Ring R
inst✝¹ : LinearOrderedField k
abv : R → k
inst✝ : IsAbsoluteValue abv
p : R[X]
h : 0 < degree p
l : Filter α
z : α → R
hz : Tendsto (abv ∘ z) l atTop
⊢ ↑(RingHom.id R) (leadingCoeff p) ≠ 0
exact (mt leadingCoeff_eq_zero.1 (ne_zero_of_degree_gt h))