mathlib3 documentation

analysis.complex.polynomial

The fundamental theorem of algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves that every nonconstant complex polynomial has a root using Liouville's theorem.

As a consequence, the complex numbers are algebraically closed.

source
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

source
@[protected, instance]
def complex.is_alg_closed  :
is_alg_closed ℂ