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 #

theorem gal_C_isSolvable {F : Type u_1} [Field F] (x : F) :
IsSolvable (Polynomial.Gal (Polynomial.C x))
theorem gal_X_isSolvable {F : Type u_1} [Field F] :
IsSolvable (Polynomial.Gal Polynomial.X)
theorem gal_X_sub_C_isSolvable {F : Type u_1} [Field F] (x : F) :
IsSolvable (Polynomial.Gal (Polynomial.X - Polynomial.C x))
theorem gal_X_pow_isSolvable {F : Type u_1} [Field F] (n : ) :
IsSolvable (Polynomial.Gal (Polynomial.X ^ n))
theorem gal_X_pow_sub_one_isSolvable {F : Type u_1} [Field F] (n : ) :
IsSolvable (Polynomial.Gal (Polynomial.X ^ n - 1))
theorem gal_X_pow_sub_C_isSolvable_aux {F : Type u_1} [Field F] (n : ) (a : F) (h : Polynomial.Splits (RingHom.id F) (Polynomial.X ^ n - 1)) :
IsSolvable (Polynomial.Gal (Polynomial.X ^ n - Polynomial.C a))
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.Splits i (Polynomial.X ^ n - Polynomial.C a)) :
Polynomial.Splits i (Polynomial.X ^ n - 1)
theorem gal_X_pow_sub_C_isSolvable {F : Type u_1} [Field F] (n : ) (x : F) :
IsSolvable (Polynomial.Gal (Polynomial.X ^ n - Polynomial.C x))
inductive IsSolvableByRad (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] :
EProp

Inductive definition of solvable by radicals

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

    The intermediate field of solvable-by-radicals elements

    Instances For
      theorem solvableByRad.induction {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (P : { x // x solvableByRad F E }Prop) (base : (α : F) → P (↑(algebraMap F { x // x solvableByRad F E }) α)) (add : (α β : { x // x solvableByRad F E }) → P αP βP (α + β)) (neg : (α : { x // x solvableByRad F E }) → P αP (-α)) (mul : (α β : { x // x solvableByRad F E }) → P αP βP (α * β)) (inv : (α : { x // x solvableByRad F E }) → P αP α⁻¹) (rad : (α : { x // x solvableByRad F E }) → (n : ) → n 0P (α ^ n)P α) (α : { x // x solvableByRad F E }) :
      P α
      theorem solvableByRad.isIntegral {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : { x // x solvableByRad F E }) :
      def solvableByRad.P {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : { x // x solvableByRad F E }) :

      The statement to be proved inductively

      Instances For
        theorem solvableByRad.induction3 {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : { x // x solvableByRad F E }} {n : } (hn : n 0) (hα : solvableByRad.P (α ^ n)) :

        An auxiliary induction lemma, which is generalized by solvableByRad.isSolvable.

        theorem solvableByRad.induction2 {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : { x // x solvableByRad F E }} {β : { x // x solvableByRad F E }} {γ : { x // x solvableByRad F E }} (hγ : γ Fα, β) (hα : solvableByRad.P α) (hβ : solvableByRad.P β) :

        An auxiliary induction lemma, which is generalized by solvableByRad.isSolvable.

        theorem solvableByRad.induction1 {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : { x // x solvableByRad F E }} {β : { x // x solvableByRad F E }} (hβ : β Fα) (hα : solvableByRad.P α) :

        An auxiliary induction lemma, which is generalized by solvableByRad.isSolvable.

        theorem solvableByRad.isSolvable {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : { x // x solvableByRad F E }) :
        theorem solvableByRad.isSolvable' {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α : IsSolvableByRad F α) :

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