The Abel-Ruffini Theorem #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
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 #
solvable_by_rad F E : the intermediate field of solvable-by-radicals elements
Main results #
- the Abel-Ruffini Theorem
solvable_by_rad.is_solvable' : An irreducible polynomial with a root
that is solvable by radicals has a solvable Galois group.
Inductive definition of solvable by radicals
The intermediate field of solvable-by-radicals elements
The statement to be proved inductively
Abel-Ruffini Theorem (one direction): An irreducible polynomial with an
is_solvable_by_rad root has solvable Galois group