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 : ℕ) : Polynomial R

A quintic polynomial that we will show is irreducible

@[simp]

theorem AbelRuffini.map_Phi {R : Type u_2} [CommRing R] (a : ℕ) (b : ℕ) {S : Type u_1} [CommRing S] (f : R →+* S) : Polynomial.map f (AbelRuffini.Φ R a b) = AbelRuffini.Φ S a b

@[simp]

theorem AbelRuffini.coeff_zero_Phi {R : Type u_1} [CommRing R] (a : ℕ) (b : ℕ) : Polynomial.coeff (AbelRuffini.Φ R a b) 0 = ↑b

@[simp]

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

theorem AbelRuffini.degree_Phi {R : Type u_1} [CommRing R] (a : ℕ) (b : ℕ) [Nontrivial R] : Polynomial.degree (AbelRuffini.Φ R a b) = ↑5

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

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

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

theorem AbelRuffini.irreducible_Phi (a : ℕ) (b : ℕ) (p : ℕ) (hp : Nat.Prime p) (hpa : p ∣ a) (hpb : p ∣ b) (hp2b : ¬p ^ 2 ∣ b) : Irreducible (AbelRuffini.Φ ℚ a b)

theorem AbelRuffini.real_roots_Phi_le (a : ℕ) (b : ℕ) : Fintype.card ↑(Polynomial.rootSet (AbelRuffini.Φ ℚ a b) ℝ) ≤ 3

theorem AbelRuffini.real_roots_Phi_ge_aux (a : ℕ) (b : ℕ) (hab : b < a) : ∃ x y, x ≠ y ∧ ↑(Polynomial.aeval x) (AbelRuffini.Φ ℚ a b) = 0 ∧ ↑(Polynomial.aeval y) (AbelRuffini.Φ ℚ a b) = 0

theorem AbelRuffini.real_roots_Phi_ge (a : ℕ) (b : ℕ) (hab : b < a) : 2 ≤ Fintype.card ↑(Polynomial.rootSet (AbelRuffini.Φ ℚ a b) ℝ)

theorem AbelRuffini.complex_roots_Phi (a : ℕ) (b : ℕ) (h : Polynomial.Separable (AbelRuffini.Φ ℚ a b)) : Fintype.card ↑(Polynomial.rootSet (AbelRuffini.Φ ℚ a b) ℂ) = 5

theorem AbelRuffini.gal_Phi (a : ℕ) (b : ℕ) (hab : b < a) (h_irred : Irreducible (AbelRuffini.Φ ℚ a b)) : Function.Bijective ↑(Polynomial.Gal.galActionHom (AbelRuffini.Φ ℚ a b) ℂ)

theorem AbelRuffini.not_solvable_by_rad (a : ℕ) (b : ℕ) (p : ℕ) (x : ℂ) (hx : ↑(Polynomial.aeval x) (AbelRuffini.Φ ℚ a b) = 0) (hab : b < a) (hp : Nat.Prime p) (hpa : p ∣ a) (hpb : p ∣ b) (hp2b : ¬p ^ 2 ∣ b) : ¬IsSolvableByRad ℚ x

theorem AbelRuffini.not_solvable_by_rad' (x : ℂ) (hx : ↑(Polynomial.aeval x) (AbelRuffini.Φ ℚ 4 2) = 0) : ¬IsSolvableByRad ℚ x

theorem AbelRuffini.exists_not_solvable_by_rad : ∃ x, IsAlgebraic ℚ x ∧ ¬IsSolvableByRad ℚ x

Abel-Ruffini Theorem