package coq-mathcomp-odd-order

The formal proof of the Feit-Thompson theorem.

From mathcomp Require Import all_ssreflect all_fingroup all_solvable PFsection14.

Check Feit_Thompson. : forall (gT : finGroupType) (G : {group gT}), odd #|G| -> solvable G

From mathcomp Require Import all_ssreflect all_fingroup all_solvable stripped_odd_order_theorem.

Check stripped_Odd_Order. : forall (T : Type) (mul : T -> T -> T) (one : T) (inv : T -> T) (G : T -> Type) (n : natural), group_axioms T mul one inv -> group T mul one inv G -> finite_of_order T G n -> odd n -> solvable_group T mul one inv G