The fundamental theorem of algebra #
This file proves that every nonconstant complex polynomial has a root using Liouville's theorem.
As a consequence, the complex numbers are algebraically closed.
theorem
Complex.exists_root
{f : Polynomial ℂ}
(hf : 0 < Polynomial.degree f)
:
∃ (z : ℂ), Polynomial.IsRoot f z
Fundamental theorem of algebra: every non constant complex polynomial has a root