Feit–Thompson theorem

Remarks

An equivalent form: every finite non-abelian simple group has even order. Indeed, a finite group is solvable exactly when all its composition factors are cyclic of prime order, and every composition factor of a group of odd order has odd order. The proof, published by Walter Feit and John Thompson in 1963, fills a whole issue of a journal and combines local analysis of subgroups with character theory. A formal proof was completed in the Coq proof assistant in 2012. The hypothesis of odd order is necessary: the alternating group $A_5$ has order $60$ and is not solvable. For example, every group of order $3 \cdot 5 \cdot 7 \cdot 11 = 1155$ is solvable, although Burnside's theorem on groups of order $p^a q^b$ does not apply to it.

Going deeper

For a student

By Cauchy's theorem, a non-abelian finite simple group therefore contains involutions, that is, elements of order $2$. This opened the way to studying simple groups through the centralisers of their involutions, the main strategy of the classification of finite simple groups. The Brauer–Fowler theorem shows that the centraliser of an involution limits the size of the simple group.