Documentation

Mathlib.Analysis.Complex.Polynomial

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.

source
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

source
instance Complex.isAlgClosed :
IsAlgClosed ℂ
Equations
source
theorem Polynomial.Gal.splits_ℚ_ℂ {p : Polynomial ℚ} :
Fact (Polynomial.Splits (algebraMap ℚ ℂ) p)
source
theorem Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv (p : Polynomial ℚ) :
(p.rootSet ℂ).toFinset.card = (p.rootSet ℝ).toFinset.card + ((Polynomial.Gal.galActionHom p ℂ) ((Polynomial.Gal.restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))).support.card

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

source
theorem Polynomial.Gal.galActionHom_bijective_of_prime_degree {p : Polynomial ℚ} (p_irr : Irreducible p) (p_deg : p.natDegree.Prime) (p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2) :
Function.Bijective ⇑(Polynomial.Gal.galActionHom p ℂ)

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

source
theorem Polynomial.Gal.galActionHom_bijective_of_prime_degree' {p : Polynomial ℚ} (p_irr : Irreducible p) (p_deg : p.natDegree.Prime) (p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)) (p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3) :
Function.Bijective ⇑(Polynomial.Gal.galActionHom p ℂ)

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

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

source
theorem Irreducible.degree_le_two {p : Polynomial ℝ} (hp : Irreducible p) :
p.degree ≤ 2

An irreducible real polynomial has degree at most two.

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

An irreducible real polynomial has natural degree at most two.

source
@[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.