mathlib documentation

analysis.complex.polynomial

The fundamental theorem of algebra

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

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

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