Formalising the Feit-Thompson Theorem:

completed on September 20, 2012

current version: April 20, 2014


Book  I: Local Analysis for The Odd Order Theorem by Helmut Bender, George Glauberman
Book II: Character Theory for The Odd Order Theorem by Thomas Peterfalvi

Index

Local Analysis for The Odd Order Theorem

by Helmut Bender, George Glauberman

Chapter I. Preliminary Results

Chapter II. The Uniqueness Theorem

Chapter III. Maximal Subgroups

Chapter IV. The Family of All Maximal Subgroups of G

Appendices

  • Appendix A. Prerequisites and p-Stability
  • 100%

    A.1, A.2, A.3, A.4(a), A.4(b), A.4(c), A.5(a), A.5(b)

  • Appendix B. The Puig Subgroup
  • 100%

    B.1(a), B.1(b), B.1(c), B.1(d), B.1(e), B.1(f), B.1(g), B.2, B.3, B.4(a), B.4(b)

  • Appendix C. The Final Contradiction
  • 100%

    I, V, VII, VIII, IX, X, XI, C.1, C.2, C.3.1 C.3.2 C.3.3 C.3.4

    Character Theory for The Odd Order Theorem

    by Thomas Peterfalvi

    Part I Character Theory for the Odd Order Theorem

    1. Preliminary Results from Character Theory
    2. 100%

      1.1, 1.2, 1.3(a), 1.3(b), 1.4, 1.5(a), 1.5(b), 1.5(c), 1.5(d), 1.5(e), 1.6(a), 1.6(b), 1.7(a) , 1.7(b) , 1.7(c) , 1.8, 1.9(a) , 1.9(b) , 1.10(a) 1.10(b)

    3. The Dade Isometry
    4. 100%

      2.1, 2.2, 2.3, 2.4, 2.5, 2.6(a), 2.6(b), 2.7(a), 2.7(b), 2.8, 2.10, 2.10.1, 2.10.2, 2.10.3, 2.11

    5. TI-Subsets with Cyclic Normalizers
    6. 100%

      3.2, 3.4, 3.5, 3.7, 3.8, 3.9(a), 3.9(b), 3.9(c)

    7. The Dade Isometry for a Certain Type of Subgroup
    8. 100%

      4.1, 4.3(a), 4.3(b, c), 4.3(d), 4.4, 4.5(a), 4.5(b), 4.7, 4.8, 4.9, 4.10

    9. Coherence
    10. 100%

      5.3(a), 5.3(b), 5.4, 5.5, 5.6, 5.7, 5.8, 5.9(a), 5.9(b)

    11. Some Coherence Theorems
    12. 100%

      6.2, 6.3, 6.5, 6.6, 6.7, 6.8

    13. Non-existence of a Certain Type of Group of Odd Order
    14. 100%

      7.2(a), 7.2(b), 7.3, 7.5, 7.7, 7.8, 7.9, 7.10, 7.11

    15. Structure of a Minimal Simple Group of Odd Order
    16. 100%

      8.2, 8.5, 8.8, 8.9, 8.11, 8.12, 8.13, 8.15, 8.16, 8.17, 8.18

    17. On the Maximal Subgroups of G of Types II, III and IV
    18. 100%

      9.1, 9.3, 9.4, 9.6, 9.7(a), 9.7(b), 9.8(a -- d) , 9.9(a -- c) , 9.10 , 9.11 ,

    19. Maximal Subgroups of Types III, IV and V
    20. 100%

      10.2, 10.3, 10.5, 10.6(a), 10.6(b), 10.7, 10.8, 10.9, 10.10, 10.11

    21. Maximal Subgroups of Types III and IV
    22. 100%

      11.1 , 11.3 , 11.4 , 11.5 , 11.6 , 11.7 , 11.8 , 11.9

    23. Maximal Subgroups of Types I
    24. 100%

      12.2(a) , 12.2(b) , 12.3 , 12.4 , 12.5 , 12.6 , 12.7 , 12.9 , 12.10 , 12.11 , 12.12 , 12.14 , 12.15 , 12.16 , 12.17

    25. The Subgroups S and T
    26. 100%

      13.2, 13.3(a), 13.3(b), 13.3(c), 13.4, 13.5(a b c), 13.6, 13.7, 13.8, 13.9(a), 13.9(b), 13.10, 13.11(a b c), 13.12, 13.13, 13.14, 13.15, 13.16, 13.17(a b c) , 13.18(a b c d), 13.19(a b c)

    27. Non-existence of G
    28. 100%

      14.2 , 14.4 , 14.5 , 14.6 , 14.7 , 14.8(a) , 14.8(b) , 14.9 , 14.11 , 14.12 , 14.14 , 14.15 , 14.16