The fundamental theorem of algebra
This file proves that every nonconstant complex polynomial has a root.
theorem
complex.exists_forall_abs_polynomial_eval_le
(p : polynomial ℂ) :
∃ (x : ℂ), ∀ (y : ℂ), complex.abs (polynomial.eval x p) ≤ complex.abs (polynomial.eval y p)
The fundamental theorem of algebra. Every non constant complex polynomial has a root