# Documentation

Archive.Wiedijk100Theorems.AbelRuffini

# 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

Instances For
@[simp]
theorem AbelRuffini.map_Phi {R : Type u_2} [] (a : ) (b : ) {S : Type u_1} [] (f : R →+* S) :
@[simp]
theorem AbelRuffini.coeff_zero_Phi {R : Type u_1} [] (a : ) (b : ) :
@[simp]
theorem AbelRuffini.coeff_five_Phi {R : Type u_1} [] (a : ) (b : ) :
theorem AbelRuffini.degree_Phi {R : Type u_1} [] (a : ) (b : ) [] :
theorem AbelRuffini.natDegree_Phi {R : Type u_1} [] (a : ) (b : ) [] :
= 5
theorem AbelRuffini.leadingCoeff_Phi {R : Type u_1} [] (a : ) (b : ) [] :
= 1
theorem AbelRuffini.monic_Phi {R : Type u_1} [] (a : ) (b : ) [] :
theorem AbelRuffini.irreducible_Phi (a : ) (b : ) (p : ) (hp : ) (hpa : p a) (hpb : p b) (hp2b : ¬p ^ 2 b) :
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) :
theorem AbelRuffini.complex_roots_Phi (a : ) (b : ) (h : ) :
Fintype.card ↑() = 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 : ) (hpa : p a) (hpb : p b) (hp2b : ¬p ^ 2 b) :
theorem AbelRuffini.not_solvable_by_rad' (x : ) (hx : ↑() () = 0) :

Abel-Ruffini Theorem