# mathlibdocumentation

mathlib-archive / 100-theorems-list.16_abel_ruffini

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

The main ingredients are:

• solvable_by_rad.is_solvable' in field_theory/abel_ruffini : an irreducible polynomial with an is_solvable_by_rad root has solvable Galois group
• gal_action_hom_bijective_of_prime_degree' in field_theory/polynomial_galois_group : an irreducible polynomial of prime degree with 1-3 non-real roots has full Galois group
• equiv.perm.not_solvable in group_theory/solvable : the symmetric group is not solvable

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

noncomputable def abel_ruffini.Φ (R : Type u_1) [comm_ring R] (a b : ) :

A quintic polynomial that we will show is irreducible

Equations
• b =
@[simp]
theorem abel_ruffini.map_Phi {R : Type u_1} [comm_ring R] (a b : ) {S : Type u_2} [comm_ring S] (f : R →+* S) :
a b) = b
@[simp]
theorem abel_ruffini.coeff_zero_Phi {R : Type u_1} [comm_ring R] (a b : ) :
a b).coeff 0 = b
@[simp]
theorem abel_ruffini.coeff_five_Phi {R : Type u_1} [comm_ring R] (a b : ) :
a b).coeff 5 = 1
theorem abel_ruffini.degree_Phi {R : Type u_1} [comm_ring R] (a b : ) [nontrivial R] :
a b).degree = 5
theorem abel_ruffini.nat_degree_Phi {R : Type u_1} [comm_ring R] (a b : ) [nontrivial R] :
a b).nat_degree = 5
theorem abel_ruffini.leading_coeff_Phi {R : Type u_1} [comm_ring R] (a b : ) [nontrivial R] :
theorem abel_ruffini.monic_Phi {R : Type u_1} [comm_ring R] (a b : ) [nontrivial R] :
a b).monic
theorem abel_ruffini.irreducible_Phi (a b p : ) (hp : nat.prime p) (hpa : p a) (hpb : p b) (hp2b : ¬p ^ 2 b) :
theorem abel_ruffini.real_roots_Phi_ge_aux (a b : ) (hab : b < a) :
(x y : ), x y b) = 0 b) = 0
theorem abel_ruffini.real_roots_Phi_ge (a b : ) (hab : b < a) :
theorem abel_ruffini.gal_Phi (a b : ) (hab : b < a) (h_irred : irreducible b)) :
theorem abel_ruffini.not_solvable_by_rad (a b p : ) (x : ) (hx : b) = 0) (hab : b < a) (hp : nat.prime p) (hpa : p a) (hpb : p b) (hp2b : ¬p ^ 2 b) :
theorem abel_ruffini.not_solvable_by_rad' (x : ) (hx : 2) = 0) :

Abel-Ruffini Theorem