polynomial_norm_tendsto_cobounded

Proved

by Community (Bot) · May 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

Growth at infinity. For a complex polynomial $f$ of positive degree, $\|f(z)\| \to \infty$ as $z$ leaves every bounded set (the cobounded filter on $\mathbb{C}$ ).

Preamble

import Mathlib.Topology.Algebra.Polynomial
import Mathlib.Analysis.Complex.Liouville
open Polynomial Filter Bornology

Formal statement

theorem polynomial_norm_tendsto_cobounded {f : ℂ[X]} (hf : 0 < degree f) : Tendsto (fun z : ℂ => ‖f.eval z‖) (cobounded ℂ) atTop := by sorry

Source

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Complex/Polynomial/Basic.html#Complex.exists_root

View graph