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 isSolvable_gal_of_irreducible: An irreducible polynomial with a root that is solvable by radicals has a solvable Galois group.

theorem gal_zero_isSolvable {F : Type u_1} [Field F] : IsSolvable (Polynomial.Gal 0)

theorem gal_one_isSolvable {F : Type u_1} [Field F] : IsSolvable (Polynomial.Gal 1)

theorem gal_C_isSolvable {F : Type u_1} [Field F] (x : F) : IsSolvable (Polynomial.C x).Gal

theorem gal_X_isSolvable {F : Type u_1} [Field F] : IsSolvable Polynomial.X.Gal

theorem gal_X_sub_C_isSolvable {F : Type u_1} [Field F] (x : F) : IsSolvable (Polynomial.X - Polynomial.C x).Gal

theorem gal_X_pow_isSolvable {F : Type u_1} [Field F] (n : ℕ) : IsSolvable (Polynomial.X ^ n).Gal

theorem gal_mul_isSolvable {F : Type u_1} [Field F] {p q : Polynomial F} : IsSolvable p.Gal → IsSolvable q.Gal → IsSolvable (p * q).Gal

theorem gal_prod_isSolvable {F : Type u_1} [Field F] {s : Multiset (Polynomial F)} (hs : ∀ p ∈ s, IsSolvable p.Gal) : IsSolvable s.prod.Gal

theorem gal_isSolvable_of_splits {F : Type u_1} [Field F] {p q : Polynomial F} : Fact (Polynomial.map (algebraMap F q.SplittingField) p).Splits → ∀ (hq : IsSolvable q.Gal), IsSolvable p.Gal

theorem gal_isSolvable_tower {F : Type u_1} [Field F] (p q : Polynomial F) (hpq : (Polynomial.map (algebraMap F q.SplittingField) p).Splits) (hp : IsSolvable p.Gal) (hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal) : IsSolvable q.Gal

theorem gal_X_pow_sub_one_isSolvable {F : Type u_1} [Field F] (n : ℕ) : IsSolvable (Polynomial.X ^ n - 1).Gal

theorem gal_X_pow_sub_C_isSolvable_aux {F : Type u_1} [Field F] (n : ℕ) (a : F) (h : (Polynomial.map (RingHom.id F) (Polynomial.X ^ n - 1)).Splits) : IsSolvable (Polynomial.X ^ n - Polynomial.C a).Gal

theorem splits_X_pow_sub_one_of_X_pow_sub_C {F : Type u_3} [Field F] {E : Type u_4} [Field E] (i : F →+* E) (n : ℕ) {a : F} (ha : a ≠ 0) (h : (Polynomial.map i (Polynomial.X ^ n - Polynomial.C a)).Splits) : (Polynomial.map i (Polynomial.X ^ n - 1)).Splits

theorem gal_X_pow_sub_C_isSolvable {F : Type u_1} [Field F] (n : ℕ) (x : F) : IsSolvable (Polynomial.X ^ n - Polynomial.C x).Gal

def solvableByRad (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] : IntermediateField F E

The intermediate field of elements solvable by radicals, defined as the smallest subfield which is closed under n-th roots.

@[deprecated solvableByRad (since := "2026-02-28")]

inductive IsSolvableByRad (F : Type u_1) {E : Type u_2} [Field F] [Field E] [Algebra F E] : E → Prop

Inductive definition of solvable by radicals

• base {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (α : F) : IsSolvableByRad F ((algebraMap F E) α)
• add {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (α β : E) : IsSolvableByRad F α → IsSolvableByRad F β → IsSolvableByRad F (α + β)
• neg {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (α : E) : IsSolvableByRad F α → IsSolvableByRad F (-α)
• mul {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (α β : E) : IsSolvableByRad F α → IsSolvableByRad F β → IsSolvableByRad F (α * β)
• inv {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (α : E) : IsSolvableByRad F α → IsSolvableByRad F α⁻¹
• rad {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (α : E) (n : ℕ) (hn : n ≠ 0) : IsSolvableByRad F (α ^ n) → IsSolvableByRad F α

theorem solvableByRad_le {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {s : IntermediateField F E} (H : ∀ (x : E) (n : ℕ), n ≠ 0 → x ^ n ∈ s → x ∈ s) : solvableByRad F E ≤ s

theorem solvableByRad.rad_mem {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {x : E} {n : ℕ} (hn : n ≠ 0) (hx : x ^ n ∈ solvableByRad F E) : x ∈ solvableByRad F E

theorem solvableByRad_le_algClosure (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] : solvableByRad F E ≤ algebraicClosure F E

theorem isAlgebraic_solvableByRad {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] : (solvableByRad F E).IsAlgebraic

theorem isIntegral_of_mem_solvableByRad {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {x : E} (hx : x ∈ solvableByRad F E) : IsIntegral F x

@[deprecated isIntegral_of_mem_solvableByRad (since := "2026-02-28")]

theorem solvableByRad.isIntegral {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {x : E} (hx : x ∈ solvableByRad F E) : IsIntegral F x

Alias of isIntegral_of_mem_solvableByRad.

theorem solvableByRad.induction {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (motive : (x : E) → x ∈ solvableByRad F E → Prop) (mem : ∀ (x : F), motive ((algebraMap F E) x) ⋯) (add : ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x + y) ⋯) (mul : ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x * y) ⋯) (rad : ∀ (n : ℕ) (x : E) (hn : n ≠ 0) (hx : x ^ n ∈ solvableByRad F E), motive (x ^ n) hx → motive x ⋯) {x : E} (hx : x ∈ solvableByRad F E) : motive x hx

An induction principle for solvableByRad.

theorem isSolvable_gal_minpoly {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {x : E} (hx : x ∈ solvableByRad F E) : IsSolvable (minpoly F x).Gal

@[deprecated isSolvable_gal_minpoly (since := "2026-02-28")]

theorem solvableByRad.isSolvable {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {x : E} (hx : x ∈ solvableByRad F E) : IsSolvable (minpoly F x).Gal

Alias of isSolvable_gal_minpoly.

theorem isSolvable_gal_of_irreducible {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {x : E} (hx : x ∈ solvableByRad F E) {q : Polynomial F} (q_irred : Irreducible q) (q_aeval : (Polynomial.aeval x) q = 0) : IsSolvable q.Gal

Abel-Ruffini Theorem (one direction): An irreducible polynomial with a solvableByRad root has a solvable Galois group.

@[deprecated isSolvable_gal_of_irreducible (since := "2026-02-28")]

theorem solvableByRad.isSolvable' {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {x : E} (hx : x ∈ solvableByRad F E) {q : Polynomial F} (q_irred : Irreducible q) (q_aeval : (Polynomial.aeval x) q = 0) : IsSolvable q.Gal

Alias of isSolvable_gal_of_irreducible.

---

Abel-Ruffini Theorem (one direction): An irreducible polynomial with a solvableByRad root has a solvable Galois group.