Construction of an algebraic number that is not solvable by radicals.

The main ingredients are:

• solvableByRad.isSolvable' in Mathlib/FieldTheory/AbelRuffini.lean : an irreducible polynomial with an IsSolvableByRad root has solvable Galois group
• galActionHom_bijective_of_prime_degree' in Mathlib/FieldTheory/PolynomialGaloisGroup.lean : an irreducible polynomial of prime degree with 1-3 non-real roots has full Galois group
• Equiv.Perm.not_solvable in Mathlib/GroupTheory/Solvable.lean : the symmetric group is not solvable

Then all that remains is the construction of a specific polynomial satisfying the conditions of galActionHom_bijective_of_prime_degree', which is done in this file.

noncomputable def AbelRuffini.Φ (R : Type u_1) [CommRing R] (a b : Nat) : Polynomial R

A quintic polynomial that we will show is irreducible

Equations

• Eq (AbelRuffini.Φ R a b) (HAdd.hAdd (HSub.hSub (HPow.hPow Polynomial.X 5) (HMul.hMul (DFunLike.coe Polynomial.C a.cast) Polynomial.X)) (DFunLike.coe Polynomial.C b.cast))

theorem AbelRuffini.map_Phi {R : Type u_1} [CommRing R] (a b : Nat) {S : Type u_2} [CommRing S] (f : RingHom R S) : Eq (Polynomial.map f (Φ R a b)) (Φ S a b)

theorem AbelRuffini.coeff_zero_Phi {R : Type u_1} [CommRing R] (a b : Nat) : Eq ((Φ R a b).coeff 0) b.cast

theorem AbelRuffini.coeff_five_Phi {R : Type u_1} [CommRing R] (a b : Nat) : Eq ((Φ R a b).coeff 5) 1

theorem AbelRuffini.degree_Phi {R : Type u_1} [CommRing R] (a b : Nat) [Nontrivial R] : Eq (Φ R a b).degree (Nat.cast 5)

theorem AbelRuffini.natDegree_Phi {R : Type u_1} [CommRing R] (a b : Nat) [Nontrivial R] : Eq (Φ R a b).natDegree 5

theorem AbelRuffini.leadingCoeff_Phi {R : Type u_1} [CommRing R] (a b : Nat) [Nontrivial R] : Eq (Φ R a b).leadingCoeff 1

theorem AbelRuffini.monic_Phi {R : Type u_1} [CommRing R] (a b : Nat) [Nontrivial R] : (Φ R a b).Monic

theorem AbelRuffini.irreducible_Phi (a b p : Nat) (hp : Nat.Prime p) (hpa : Dvd.dvd p a) (hpb : Dvd.dvd p b) (hp2b : Not (Dvd.dvd (HPow.hPow p 2) b)) : Irreducible (Φ Rat a b)

theorem AbelRuffini.real_roots_Phi_le (a b : Nat) : LE.le (Fintype.card ((Φ Rat a b).rootSet Real).Elem) 3

theorem AbelRuffini.real_roots_Phi_ge_aux (a b : Nat) (hab : LT.lt b a) : Exists fun (x : Real) => Exists fun (y : Real) => And (Ne x y) (And (Eq (DFunLike.coe (Polynomial.aeval x) (Φ Rat a b)) 0) (Eq (DFunLike.coe (Polynomial.aeval y) (Φ Rat a b)) 0))

theorem AbelRuffini.real_roots_Phi_ge (a b : Nat) (hab : LT.lt b a) : LE.le 2 (Fintype.card ((Φ Rat a b).rootSet Real).Elem)

theorem AbelRuffini.complex_roots_Phi (a b : Nat) (h : (Φ Rat a b).Separable) : Eq (Fintype.card ((Φ Rat a b).rootSet Complex).Elem) 5

theorem AbelRuffini.gal_Phi (a b : Nat) (hab : LT.lt b a) (h_irred : Irreducible (Φ Rat a b)) : Function.Bijective (DFunLike.coe (Polynomial.Gal.galActionHom (Φ Rat a b) Complex))

theorem AbelRuffini.not_solvable_by_rad (a b p : Nat) (x : Complex) (hx : Eq (DFunLike.coe (Polynomial.aeval x) (Φ Rat a b)) 0) (hab : LT.lt b a) (hp : Nat.Prime p) (hpa : Dvd.dvd p a) (hpb : Dvd.dvd p b) (hp2b : Not (Dvd.dvd (HPow.hPow p 2) b)) : Not (IsSolvableByRad Rat x)

theorem AbelRuffini.not_solvable_by_rad' (x : Complex) (hx : Eq (DFunLike.coe (Polynomial.aeval x) (Φ Rat 4 2)) 0) : Not (IsSolvableByRad Rat x)

theorem AbelRuffini.exists_not_solvable_by_rad : Exists fun (x : Complex) => And (IsAlgebraic Rat x) (Not (IsSolvableByRad Rat x))

Abel-Ruffini Theorem