package coq-mathcomp-odd-order
The formal proof of the Feit-Thompson theorem
Install
Dune Dependency
Authors
Maintainers
Sources
mathcomp-odd-order.2.1.0.tar.gz
sha256=2bc2f282a4b5712534cd8a6363dac472687ab67eedcc9bbee7d7f46ae748de9a
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
Tags
keyword:finite groups keyword:Feit Thompson theorem keyword:small scale reflection keyword:mathematical components keyword:odd order theoremPublished: 04 Jan 2025
Dependencies (1)
-
coq-mathcomp-character
>= "2.1.0" & < "2.4~"
Dev Dependencies
None
Used by
None
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page