mathlib documentation

analysis.complex.polynomial

The fundamental theorem of algebra

This file proves that every nonconstant complex polynomial has a root.

source
theorem complex.exists_forall_abs_polynomial_eval_le (p : polynomial ℂ) :
∃ (x : ℂ), ∀ (y : ℂ), complex.abs (polynomial.eval x p) ≤ complex.abs (polynomial.eval y p)

source
theorem complex.exists_root {f : polynomial ℂ} (hf : 0 < f.degree) :
∃ (z : ℂ), f.is_root z

The fundamental theorem of algebra. Every non constant complex polynomial has a root