mathlib documentation

topology.algebra.polynomial

source
theorem polynomial.tendsto_infinity {α : Type u_1} {β : Type u_2} [comm_ring α] [discrete_linear_ordered_field β] (abv : α → β) [is_absolute_value abv] {p : polynomial α} (h : 0 < p.degree) (x : β) :
∃ (r : β) (H : r > 0), ∀ (z : α), r < abv z → x < abv (polynomial.eval z p)

source
theorem polynomial.continuous_eval {α : Type u_1} [comm_semiring α] [topological_space α] [topological_semiring α] (p : polynomial α) :
continuous (λ (x : α), polynomial.eval x p)