Construction of an algebraic number that is not solvable by radicals. #
The main ingredients are:
Mathlib/FieldTheory/AbelRuffini.lean: an irreducible polynomial with an
IsSolvableByRadroot has solvable Galois group
Mathlib/FieldTheory/PolynomialGaloisGroup.lean: an irreducible polynomial of prime degree with 1-3 non-real roots has full Galois group
Mathlib/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.