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

instance Complex.isAlgClosed : IsAlgClosed ℂ

theorem Polynomial.Gal.splits_ℚ_ℂ {p : Polynomial ℚ} : Fact (Polynomial.Splits (algebraMap ℚ ℂ) p)

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

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) : Function.Bijective ⇑(Polynomial.Gal.galActionHom p ℂ)

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) : Function.Bijective ⇑(Polynomial.Gal.galActionHom p ℂ)

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.