# 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) [] (a : ) (b : ) :

A quintic polynomial that we will show is irreducible

Equations
• = Polynomial.X ^ 5 - Polynomial.C a * Polynomial.X + Polynomial.C b
Instances For
@[simp]
theorem AbelRuffini.map_Phi {R : Type u_1} [] (a : ) (b : ) {S : Type u_2} [] (f : R →+* S) :
@[simp]
theorem AbelRuffini.coeff_zero_Phi {R : Type u_1} [] (a : ) (b : ) :
().coeff 0 = b
@[simp]
theorem AbelRuffini.coeff_five_Phi {R : Type u_1} [] (a : ) (b : ) :
().coeff 5 = 1
theorem AbelRuffini.degree_Phi {R : Type u_1} [] (a : ) (b : ) [] :
().degree = 5
theorem AbelRuffini.natDegree_Phi {R : Type u_1} [] (a : ) (b : ) [] :
().natDegree = 5
theorem AbelRuffini.leadingCoeff_Phi {R : Type u_1} [] (a : ) (b : ) [] :
theorem AbelRuffini.monic_Phi {R : Type u_1} [] (a : ) (b : ) [] :
().Monic
theorem AbelRuffini.irreducible_Phi (a : ) (b : ) (p : ) (hp : p.Prime) (hpa : p a) (hpb : p b) (hp2b : ¬p ^ 2 b) :
theorem AbelRuffini.real_roots_Phi_le (a : ) (b : ) :
Fintype.card (().rootSet ) 3
theorem AbelRuffini.real_roots_Phi_ge_aux (a : ) (b : ) (hab : b < a) :
∃ (x : ) (y : ), x y () () = 0 () () = 0
theorem AbelRuffini.real_roots_Phi_ge (a : ) (b : ) (hab : b < a) :
2 Fintype.card (().rootSet )
theorem AbelRuffini.complex_roots_Phi (a : ) (b : ) (h : ().Separable) :
Fintype.card (().rootSet ) = 5
theorem AbelRuffini.gal_Phi (a : ) (b : ) (hab : b < a) (h_irred : Irreducible ()) :
theorem AbelRuffini.not_solvable_by_rad (a : ) (b : ) (p : ) (x : ) (hx : () () = 0) (hab : b < a) (hp : p.Prime) (hpa : p a) (hpb : p b) (hp2b : ¬p ^ 2 b) :
theorem AbelRuffini.not_solvable_by_rad' (x : ) (hx : () () = 0) :

Abel-Ruffini Theorem