mathlib documentation

analysis.complex.polynomial

The fundamental theorem of algebra #

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

As a consequence, the complex numbers are algebraically closed.

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

Fundamental theorem of algebra: every non constant complex polynomial has a root