# mathlibdocumentation

field_theory.abel_ruffini

# 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 #

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

## Main results #

• the Abel-Ruffini Theorem solvable_by_rad.is_solvable' : An irreducible polynomial with a root that is solvable by radicals has a solvable Galois group.
theorem gal_zero_is_solvable {F : Type u_1} [field F] :
theorem gal_one_is_solvable {F : Type u_1} [field F] :
theorem gal_C_is_solvable {F : Type u_1} [field F] (x : F) :
theorem gal_X_is_solvable {F : Type u_1} [field F] :
theorem gal_X_sub_C_is_solvable {F : Type u_1} [field F] (x : F) :
theorem gal_X_pow_is_solvable {F : Type u_1} [field F] (n : ) :
theorem gal_mul_is_solvable {F : Type u_1} [field F] {p q : polynomial F} (hp : is_solvable p.gal) (hq : is_solvable q.gal) :
theorem gal_prod_is_solvable {F : Type u_1} [field F] {s : multiset (polynomial F)} (hs : ∀ (p : , p s) :
theorem gal_is_solvable_of_splits {F : Type u_1} [field F] {p q : polynomial F} (hpq : fact p)) (hq : is_solvable q.gal) :
theorem gal_is_solvable_tower {F : Type u_1} [field F] (p q : polynomial F) (hpq : p) (hp : is_solvable p.gal) (hq : is_solvable q).gal) :
theorem gal_X_pow_sub_one_is_solvable {F : Type u_1} [field F] (n : ) :
theorem gal_X_pow_sub_C_is_solvable_aux {F : Type u_1} [field F] (n : ) (a : F) (h : - 1)) :
theorem splits_X_pow_sub_one_of_X_pow_sub_C {F : Type u_1} [field F] {E : Type u_2} [field E] (i : F →+* E) (n : ) {a : F} (ha : a 0) (h : - ) :
- 1)
theorem gal_X_pow_sub_C_is_solvable {F : Type u_1} [field F] (n : ) (x : F) :
inductive is_solvable_by_rad (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] :
E → Prop
• base : ∀ {F : Type u_1} [_inst_1 : field F] {E : Type u_2} [_inst_2 : field E] [_inst_3 : E] (a : F), ( E) a)
• add : ∀ {F : Type u_1} [_inst_1 : field F] {E : Type u_2} [_inst_2 : field E] [_inst_3 : E] (a b : E), (a + b)
• neg : ∀ {F : Type u_1} [_inst_1 : field F] {E : Type u_2} [_inst_2 : field E] [_inst_3 : E] (α : E), (-α)
• mul : ∀ {F : Type u_1} [_inst_1 : field F] {E : Type u_2} [_inst_2 : field E] [_inst_3 : E] (α β : E), * β)
• inv : ∀ {F : Type u_1} [_inst_1 : field F] {E : Type u_2} [_inst_2 : field E] [_inst_3 : E] (α : E),
• rad : ∀ {F : Type u_1} [_inst_1 : field F] {E : Type u_2} [_inst_2 : field E] [_inst_3 : E] (α : E) (n : ), n 0 ^ n)

Inductive definition of solvable by radicals

def solvable_by_rad (F : Type u_1) [field F] (E : Type u_2) [field E] [ E] :

The intermediate field of solvable-by-radicals elements

Equations
theorem solvable_by_rad.induction {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (P : E) → Prop) (base : ∀ (α : F), P ( E)) α)) (add : ∀ (α β : E)), P αP βP + β)) (neg : ∀ (α : E)), P αP (-α)) (mul : ∀ (α β : E)), P αP βP * β)) (inv : ∀ (α : E)), P αP α⁻¹) (rad : ∀ (α : E)) (n : ), n 0P ^ n)P α) (α : E)) :
P α
theorem solvable_by_rad.is_integral {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (α : E)) :
α
def solvable_by_rad.P {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (α : E)) :
Prop

The statement to be proved inductively

Equations
theorem solvable_by_rad.induction3 {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {α : E)} {n : } (hn : n 0) (hα : solvable_by_rad.P ^ n)) :

An auxiliary induction lemma, which is generalized by solvable_by_rad.is_solvable.

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

An auxiliary induction lemma, which is generalized by solvable_by_rad.is_solvable.

theorem solvable_by_rad.induction1 {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {α β : E)} (hβ : β Fα) (hα : solvable_by_rad.P α) :

An auxiliary induction lemma, which is generalized by solvable_by_rad.is_solvable.

theorem solvable_by_rad.is_solvable {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (α : E)) :
theorem solvable_by_rad.is_solvable' {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {α : E} {q : polynomial F} (q_irred : irreducible q) (q_aeval : q = 0) (hα : α) :

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