Documentation

Mathlib.FieldTheory.AbelRuffini

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 #

source
theorem gal_zero_isSolvable {F : Type u_1} [Field F] :
IsSolvable (Polynomial.Gal 0)
source
theorem gal_one_isSolvable {F : Type u_1} [Field F] :
IsSolvable (Polynomial.Gal 1)
source
theorem gal_C_isSolvable {F : Type u_1} [Field F] (x : F) :
IsSolvable (Polynomial.C x).Gal
source
theorem gal_X_isSolvable {F : Type u_1} [Field F] :
IsSolvable Polynomial.X.Gal
source
theorem gal_X_sub_C_isSolvable {F : Type u_1} [Field F] (x : F) :
IsSolvable (Polynomial.X - Polynomial.C x).Gal
source
theorem gal_X_pow_isSolvable {F : Type u_1} [Field F] (n : ℕ) :
IsSolvable (Polynomial.X ^ n).Gal
source
theorem gal_mul_isSolvable {F : Type u_1} [Field F] {p q : Polynomial F} :
IsSolvable p.Gal → IsSolvable q.Gal → IsSolvable (p * q).Gal
source
theorem gal_prod_isSolvable {F : Type u_1} [Field F] {s : Multiset (Polynomial F)} (hs : ∀ p ∈ s, IsSolvable p.Gal) :
IsSolvable s.prod.Gal
source
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
source
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
source
theorem gal_X_pow_sub_one_isSolvable {F : Type u_1} [Field F] (n : ℕ) :
IsSolvable (Polynomial.X ^ n - 1).Gal
source
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
source
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
source
theorem gal_X_pow_sub_C_isSolvable {F : Type u_1} [Field F] (n : ℕ) (x : F) :
IsSolvable (Polynomial.X ^ n - Polynomial.C x).Gal
source
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.

Equations
Instances For
    source
    @[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

    Instances For
      source
      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
      source
      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
      source
      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
      source
      theorem isAlgebraic_solvableByRad {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] :
      (solvableByRad F E).IsAlgebraic
      source
      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
      source
      @[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.

      source
      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.

      source
      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
      source
      @[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.

      source
      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.

      source
      @[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.