Construction of an algebraic number that is not solvable by radicals. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
The main ingredients are:
an irreducible polynomial with an
is_solvable_by_rad root has solvable Galois group
an irreducible polynomial of prime degree with 1-3 non-real roots has full Galois group
group_theory/solvable : the symmetric group is not solvable
Then all that remains is the construction of a specific polynomial satisfying the conditions of
gal_action_hom_bijective_of_prime_degree', which is done in this file.
A quintic polynomial that we will show is irreducible