# 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.

We also provide some specific results about the Galois groups of ℚ-polynomials with specific numbers of non-real roots.

We also show that an irreducible real polynomial has degree at most two.

theorem Complex.exists_root {f : } (hf : ) :
∃ (z : ),

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

Equations

The number of complex roots equals the number of real roots plus the number of roots not fixed by complex conjugation (i.e. with some imaginary component).

theorem Polynomial.Gal.galActionHom_bijective_of_prime_degree {p : } (p_irr : ) (p_deg : ) (p_roots : = + 2) :

An irreducible polynomial of prime degree with two non-real roots has full Galois group.

theorem Polynomial.Gal.galActionHom_bijective_of_prime_degree' {p : } (p_irr : ) (p_deg : ) (p_roots1 : + 1 ) (p_roots2 : + 3) :

An irreducible polynomial of prime degree with 1-3 non-real roots has full Galois group.

theorem Polynomial.mul_star_dvd_of_aeval_eq_zero_im_ne_zero (p : ) {z : } (h0 : () p = 0) (hz : z.im 0) :
(Polynomial.X - Polynomial.C (() z)) * (Polynomial.X - Polynomial.C z)
theorem Polynomial.quadratic_dvd_of_aeval_eq_zero_im_ne_zero (p : ) {z : } (h0 : () p = 0) (hz : z.im 0) :
Polynomial.X ^ 2 - Polynomial.C (2 * z.re) * Polynomial.X + Polynomial.C (z ^ 2) p

If z is a non-real complex root of a real polynomial, then p is divisible by a quadratic polynomial.

theorem Irreducible.degree_le_two {p : } (hp : ) :

An irreducible real polynomial has degree at most two.

theorem Irreducible.natDegree_le_two {p : } (hp : ) :

An irreducible real polynomial has natural degree at most two.

@[deprecated Irreducible.natDegree_le_two]
theorem Irreducible.nat_degree_le_two {p : } (hp : ) :

Alias of Irreducible.natDegree_le_two.

An irreducible real polynomial has natural degree at most two.