# The Abel-Ruffini Theorem #

This file proves one direction of the Abel-Ruffini theorem, namely that if an element is solvable by radicals, then its minimal polynomial has solvable Galois group.

## Main definitions #

• solvableByRad F E : the intermediate field of solvable-by-radicals elements

## Main results #

• the Abel-Ruffini Theorem solvableByRad.isSolvable' : An irreducible polynomial with a root that is solvable by radicals has a solvable Galois group.
theorem gal_zero_isSolvable {F : Type u_1} [] :
theorem gal_one_isSolvable {F : Type u_1} [] :
theorem gal_C_isSolvable {F : Type u_1} [] (x : F) :
IsSolvable (Polynomial.C x).Gal
theorem gal_X_isSolvable {F : Type u_1} [] :
IsSolvable Polynomial.X.Gal
theorem gal_X_sub_C_isSolvable {F : Type u_1} [] (x : F) :
IsSolvable (Polynomial.X - Polynomial.C x).Gal
theorem gal_X_pow_isSolvable {F : Type u_1} [] (n : ) :
IsSolvable (Polynomial.X ^ n).Gal
theorem gal_mul_isSolvable {F : Type u_1} [] {p : } {q : } :
IsSolvable p.GalIsSolvable q.GalIsSolvable (p * q).Gal
theorem gal_prod_isSolvable {F : Type u_1} [] {s : } (hs : ps, IsSolvable p.Gal) :
IsSolvable s.prod.Gal
theorem gal_isSolvable_of_splits {F : Type u_1} [] {p : } {q : } :
Fact (Polynomial.Splits (algebraMap F q.SplittingField) p)IsSolvable q.GalIsSolvable p.Gal
theorem gal_isSolvable_tower {F : Type u_1} [] (p : ) (q : ) (hpq : Polynomial.Splits (algebraMap F q.SplittingField) p) (hp : IsSolvable p.Gal) (hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal) :
theorem gal_X_pow_sub_one_isSolvable {F : Type u_1} [] (n : ) :
IsSolvable (Polynomial.X ^ n - 1).Gal
theorem gal_X_pow_sub_C_isSolvable_aux {F : Type u_1} [] (n : ) (a : F) (h : Polynomial.Splits () (Polynomial.X ^ n - 1)) :
IsSolvable (Polynomial.X ^ n - Polynomial.C a).Gal
theorem splits_X_pow_sub_one_of_X_pow_sub_C {F : Type u_3} [] {E : Type u_4} [] (i : F →+* E) (n : ) {a : F} (ha : a 0) (h : Polynomial.Splits i (Polynomial.X ^ n - Polynomial.C a)) :
Polynomial.Splits i (Polynomial.X ^ n - 1)
theorem gal_X_pow_sub_C_isSolvable {F : Type u_1} [] (n : ) (x : F) :
IsSolvable (Polynomial.X ^ n - Polynomial.C x).Gal
inductive IsSolvableByRad (F : Type u_1) [] {E : Type u_2} [] [Algebra F E] :
EProp

Inductive definition of solvable by radicals

Instances For
def solvableByRad (F : Type u_1) [] (E : Type u_2) [] [Algebra F E] :

The intermediate field of solvable-by-radicals elements

Equations
• = { carrier := , mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , algebraMap_mem' := , inv_mem' := }
Instances For
theorem solvableByRad.induction {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (P : ()Prop) (base : ∀ (α : F), P ((algebraMap F ()) α)) (add : ∀ (α β : ()), P αP βP (α + β)) (neg : ∀ (α : ()), P αP (-α)) (mul : ∀ (α β : ()), P αP βP (α * β)) (inv : ∀ (α : ()), P αP α⁻¹) (rad : ∀ (α : ()) (n : ), n 0P (α ^ n)P α) (α : ()) :
P α
theorem solvableByRad.isIntegral {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (α : ()) :
def solvableByRad.P {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (α : ()) :

The statement to be proved inductively

Equations
Instances For
theorem solvableByRad.induction3 {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {α : ()} {n : } (hn : n 0) (hα : solvableByRad.P (α ^ n)) :

An auxiliary induction lemma, which is generalized by solvableByRad.isSolvable.

theorem solvableByRad.induction2 {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {α : ()} {β : ()} {γ : ()} (hγ : γ Fα, β) (hα : ) (hβ : ) :

An auxiliary induction lemma, which is generalized by solvableByRad.isSolvable.

theorem solvableByRad.induction1 {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {α : ()} {β : ()} (hβ : β Fα) (hα : ) :

An auxiliary induction lemma, which is generalized by solvableByRad.isSolvable.

theorem solvableByRad.isSolvable {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] (α : ()) :
IsSolvable (minpoly F α).Gal
theorem solvableByRad.isSolvable' {F : Type u_1} [] {E : Type u_2} [] [Algebra F E] {α : E} {q : } (q_irred : ) (q_aeval : () q = 0) (hα : ) :

Abel-Ruffini Theorem (one direction): An irreducible polynomial with an IsSolvableByRad root has solvable Galois group