Construction of an algebraic number that is not solvable by radicals. #
The main ingredients are:
solvableByRad.isSolvable'
inMathlib/FieldTheory/AbelRuffini.lean
: an irreducible polynomial with anIsSolvableByRad
root has solvable Galois groupgalActionHom_bijective_of_prime_degree'
inMathlib/FieldTheory/PolynomialGaloisGroup.lean
: an irreducible polynomial of prime degree with 1-3 non-real roots has full Galois groupEquiv.Perm.not_solvable
inMathlib/GroupTheory/Solvable.lean
: the symmetric group is not solvable
Then all that remains is the construction of a specific polynomial satisfying the conditions of
galActionHom_bijective_of_prime_degree'
, which is done in this file.
A quintic polynomial that we will show is irreducible
Instances For
@[simp]
theorem
AbelRuffini.map_Phi
{R : Type u_2}
[CommRing R]
(a : ℕ)
(b : ℕ)
{S : Type u_1}
[CommRing S]
(f : R →+* S)
:
Polynomial.map f (AbelRuffini.Φ R a b) = AbelRuffini.Φ S a b
@[simp]
theorem
AbelRuffini.coeff_zero_Phi
{R : Type u_1}
[CommRing R]
(a : ℕ)
(b : ℕ)
:
Polynomial.coeff (AbelRuffini.Φ R a b) 0 = ↑b
@[simp]
theorem
AbelRuffini.coeff_five_Phi
{R : Type u_1}
[CommRing R]
(a : ℕ)
(b : ℕ)
:
Polynomial.coeff (AbelRuffini.Φ R a b) 5 = 1
theorem
AbelRuffini.degree_Phi
{R : Type u_1}
[CommRing R]
(a : ℕ)
(b : ℕ)
[Nontrivial R]
:
Polynomial.degree (AbelRuffini.Φ R a b) = ↑5
theorem
AbelRuffini.natDegree_Phi
{R : Type u_1}
[CommRing R]
(a : ℕ)
(b : ℕ)
[Nontrivial R]
:
Polynomial.natDegree (AbelRuffini.Φ R a b) = 5
theorem
AbelRuffini.leadingCoeff_Phi
{R : Type u_1}
[CommRing R]
(a : ℕ)
(b : ℕ)
[Nontrivial R]
:
Polynomial.leadingCoeff (AbelRuffini.Φ R a b) = 1
theorem
AbelRuffini.monic_Phi
{R : Type u_1}
[CommRing R]
(a : ℕ)
(b : ℕ)
[Nontrivial R]
:
Polynomial.Monic (AbelRuffini.Φ R a b)
theorem
AbelRuffini.irreducible_Phi
(a : ℕ)
(b : ℕ)
(p : ℕ)
(hp : Nat.Prime p)
(hpa : p ∣ a)
(hpb : p ∣ b)
(hp2b : ¬p ^ 2 ∣ b)
:
Irreducible (AbelRuffini.Φ ℚ a b)
theorem
AbelRuffini.real_roots_Phi_le
(a : ℕ)
(b : ℕ)
:
Fintype.card ↑(Polynomial.rootSet (AbelRuffini.Φ ℚ a b) ℝ) ≤ 3
theorem
AbelRuffini.real_roots_Phi_ge_aux
(a : ℕ)
(b : ℕ)
(hab : b < a)
:
∃ x y, x ≠ y ∧ ↑(Polynomial.aeval x) (AbelRuffini.Φ ℚ a b) = 0 ∧ ↑(Polynomial.aeval y) (AbelRuffini.Φ ℚ a b) = 0
theorem
AbelRuffini.real_roots_Phi_ge
(a : ℕ)
(b : ℕ)
(hab : b < a)
:
2 ≤ Fintype.card ↑(Polynomial.rootSet (AbelRuffini.Φ ℚ a b) ℝ)
theorem
AbelRuffini.complex_roots_Phi
(a : ℕ)
(b : ℕ)
(h : Polynomial.Separable (AbelRuffini.Φ ℚ a b))
:
Fintype.card ↑(Polynomial.rootSet (AbelRuffini.Φ ℚ a b) ℂ) = 5
theorem
AbelRuffini.gal_Phi
(a : ℕ)
(b : ℕ)
(hab : b < a)
(h_irred : Irreducible (AbelRuffini.Φ ℚ a b))
:
theorem
AbelRuffini.not_solvable_by_rad'
(x : ℂ)
(hx : ↑(Polynomial.aeval x) (AbelRuffini.Φ ℚ 4 2) = 0)
:
Abel-Ruffini Theorem