Bender–Suzuki theorem (classification of finite simple groups with a strongly-embedded subgroup)

bender_suzuki

Submitter: Tianjiao Nie.

Notes: For a finite simple group X with a strongly-embedded subgroup M, it is PSL, PSU, or Sz.

Source: D. Gorenstein, R. Lyons, and R. Solomon, The classification of the finite simple groups, Number 2

Informal solution: Unavailable.

theorem declaration uses `sorry`bender_suzuki {X : Type*} [Group X] [Finite X] [IsSimpleGroup X]
    (M : Subgroup X) (h : LeanEval.GroupTheory.Defs.IsStronglyEmbedded M) :
    LeanEval.GroupTheory.Defs.IsSimpleBenderGroup X := byX:Type u_1inst✝²:Group Xinst✝¹:Finite Xinst✝:IsSimpleGroup XM:Subgroup Xh:IsStronglyEmbedded M⊢ IsSimpleBenderGroup X
  sorryAll goals completed! 🐙

Solved by

Not yet solved.