package coq-mathcomp-odd-order

  1. Overview
  2. No Docs
The formal proof of the Feit-Thompson theorem

Install

Dune Dependency

math-comp.github.io Edit opam file Versions (8)

Authors

  1. J
    Jeremy Avigad <>
  2. A
    Andrea Asperti <>
  3. S
    Stephane Le Roux <>
  4. Y
    Yves Bertot <>
  5. L
    Laurence Rideau <>
  6. E
    Enrico Tassi <>
  7. I
    Ioana Pasca <>
  8. G
    Georges Gonthier <>
  9. S
    Sidi Ould Biha <>
  10. C
    Cyril Cohen <>
  11. F
    Francois Garillot <>
  12. A
    Alexey Solovyev <>
  13. R
    Russell O'Connor <>
  14. L
    Laurent Théry <>
  15. A
    Assia Mahboubi <>

Maintainers

  1. M
    Mathematical Components <mathcomp-dev@sympa.inria.fr>

Sources

mathcomp-odd-order.1.10.0.tar.gz
sha256=c3ddd9f3c3882985cf01afbc72866f551cbba314f45478a248b7aec88bf8f533

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 theorem

Published: 04 Mar 2020

Dev Dependencies

None

Used by

None

Conflicts

None