Documentation

Mathlib.Analysis.Complex.Polynomial.Basic

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 : Polynomial } (hf : 0 < f.degree) :
∃ (z : ), f.IsRoot z

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

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 : Polynomial } (p_irr : Irreducible p) (p_deg : Nat.Prime p.natDegree) (p_roots : Fintype.card (p.rootSet ) = Fintype.card (p.rootSet ) + 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 : Polynomial } (p_irr : Irreducible p) (p_deg : Nat.Prime p.natDegree) (p_roots1 : Fintype.card (p.rootSet ) + 1 Fintype.card (p.rootSet )) (p_roots2 : Fintype.card (p.rootSet ) Fintype.card (p.rootSet ) + 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 : Polynomial ) {z : } (h0 : (Polynomial.aeval z) p = 0) (hz : z.im 0) :
(Polynomial.X - Polynomial.C ((starRingEnd ) z)) * (Polynomial.X - Polynomial.C z) Polynomial.map (algebraMap ) p
theorem Polynomial.quadratic_dvd_of_aeval_eq_zero_im_ne_zero (p : Polynomial ) {z : } (h0 : (Polynomial.aeval z) 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 : Polynomial } (hp : Irreducible p) :
p.degree 2

An irreducible real polynomial has degree at most two.

theorem Irreducible.natDegree_le_two {p : Polynomial } (hp : Irreducible p) :
p.natDegree 2

An irreducible real polynomial has natural degree at most two.

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

Alias of Irreducible.natDegree_le_two.


An irreducible real polynomial has natural degree at most two.