Every finite group of odd order is a solvable group.
This is due to (Feit-Thompson 62).
A fully formalized proof in Coq has been announced in (INRIA 2012)
Walter Feit, John Thompson, A solvability criterion for finite groups and some consequences, Proc. Nat. Acad. Sci. 48 (6): 968–970, 1962 (JSTOR)
INRIA, Feit-Thompson theorem has been totally checked in Coq
Last revised on September 12, 2018 at 11:21:41. See the history of this page for a list of all contributions to it.