Documentation

Archive.Wiedijk100Theorems.AbelRuffini

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

The main ingredients are:

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 : ) :

A quintic polynomial that we will show is irreducible

Instances For
    @[simp]
    theorem AbelRuffini.map_Phi {R : Type u_2} [CommRing R] (a : ) (b : ) {S : Type u_1} [CommRing S] (f : R →+* S) :
    @[simp]
    theorem AbelRuffini.coeff_zero_Phi {R : Type u_1} [CommRing R] (a : ) (b : ) :
    @[simp]
    theorem AbelRuffini.coeff_five_Phi {R : Type u_1} [CommRing R] (a : ) (b : ) :
    theorem AbelRuffini.degree_Phi {R : Type u_1} [CommRing R] (a : ) (b : ) [Nontrivial R] :
    theorem AbelRuffini.irreducible_Phi (a : ) (b : ) (p : ) (hp : Nat.Prime p) (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 ↑(Polynomial.aeval x) (AbelRuffini.Φ a b) = 0 ↑(Polynomial.aeval y) (AbelRuffini.Φ a b) = 0
    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) :