mathlib documentation

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 #

Main results #

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 : polynomial F), p sis_solvable p.gal) :
theorem gal_is_solvable_of_splits {F : Type u_1} [field F] {p q : polynomial F} (hpq : fact (polynomial.splits (algebra_map F q.splitting_field) p)) (hq : is_solvable q.gal) :
theorem gal_X_pow_sub_one_is_solvable {F : Type u_1} [field F] (n : ) :
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 : polynomial.splits i (polynomial.X ^ n - polynomial.C a)) :
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] [algebra F 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] [algebra F 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] [algebra F E] (P : (solvable_by_rad F E) → Prop) (base : ∀ (α : F), P ((algebra_map F (solvable_by_rad F E)) α)) (add : ∀ (α β : (solvable_by_rad F E)), P αP βP + β)) (neg : ∀ (α : (solvable_by_rad F E)), P αP (-α)) (mul : ∀ (α β : (solvable_by_rad F E)), P αP βP * β)) (inv : ∀ (α : (solvable_by_rad F E)), P αP α⁻¹) (rad : ∀ (α : (solvable_by_rad F E)) (n : ), n 0P ^ n)P α) (α : (solvable_by_rad F E)) :
P α
theorem solvable_by_rad.is_integral {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (α : (solvable_by_rad F E)) :
def solvable_by_rad.P {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] (α : (solvable_by_rad F 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] [algebra F E] {α : (solvable_by_rad F 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] [algebra F E] {α β γ : (solvable_by_rad F 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] [algebra F E] {α β : (solvable_by_rad F 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] [algebra F E] (α : (solvable_by_rad F E)) :
theorem solvable_by_rad.is_solvable' {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] {α : E} {q : polynomial F} (q_irred : irreducible q) (q_aeval : (polynomial.aeval α) q = 0) (hα : is_solvable_by_rad F α) :

An irreducible polynomial with an is_solvable_by_rad root has solvable Galois group