diff --git a/released/packages/coq-mathcomp-odd-order/coq-mathcomp-odd-order.2.1.0/opam b/released/packages/coq-mathcomp-odd-order/coq-mathcomp-odd-order.2.1.0/opam new file mode 100644 index 000000000..5f82c8a34 --- /dev/null +++ b/released/packages/coq-mathcomp-odd-order/coq-mathcomp-odd-order.2.1.0/opam @@ -0,0 +1,39 @@ +opam-version: "2.0" +maintainer: "Mathematical Components " +homepage: "https://math-comp.github.io/math-comp/" +bug-reports: "Mathematical Components " +dev-repo: "git+https://github.com/math-comp/odd-order" +license: "CeCILL-B" + +build: [ + [make "-j" "%{jobs}%"] +] +install: [ make "install" ] +depends: [ + "coq-mathcomp-character" {>= "2.1.0" & < "2.4~"} +] +tags: [ "keyword:finite groups" "keyword:Feit Thompson theorem" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" ] +authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ] +synopsis: "The formal proof of the Feit-Thompson theorem" +description: """ +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""" + +url { + src: "https://github.com/math-comp/odd-order/archive/mathcomp-odd-order.2.1.0.tar.gz" + checksum: "sha256=2bc2f282a4b5712534cd8a6363dac472687ab67eedcc9bbee7d7f46ae748de9a" +}