# mathlib3documentation

field_theory.abel_ruffini

# The Abel-Ruffini Theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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 0 P ^ 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