The case division

The top theorem, the module that reduces it to 9 cases, and the theorem the top theorem's proof gives for each case, in the order of the reduction's hypotheses. Each entry for a case names the proposition it proves.

TheoremCFSG.classification_finite_simple_groups#

The proof's top theorem, quoted from CFSG/Statement.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.classification_finite_simple_groups (theorem, line 4923). Proved here.

theorem classification_finite_simple_groups
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G] :
    ∃ i : TauCeti.CFSGIndex, Nonempty (G ≃* i.Group)

Its proof applies CFSG.Assembly.classification to the catalog CFSG.Assembly.InCatalog and to a theorem for each of the reduction's 9 hypotheses, in its order:

The catalog, declared in CFSG/Assembly/InCatalog.lean, line 10:

@[expose] def InCatalog : GroupProp := fun G _ => ∃ i : TauCeti.CFSGIndex, Nonempty (G ≃* i.Group)
Sources
LeanCFSG.classification_finite_simple_groups
Uses 10
Proof usesCFSG.Assembly.Reduction · CFSG.FeitThompson.isSolvable_of_odd_natCard · CFSG.Assembly.abelian_simple · CFSG.Assembly.disconnected_involution_graph · CFSG.Assembly.low_two_rank · CFSG.Assembly.component_dichotomy · CFSG.Assembly.component_type · CFSG.Assembly.quasithin · CFSG.Assembly.rank_three_even · CFSG.Assembly.large_even

TheoremCFSG.Assembly.Reduction#

The module CFSG.Assembly.Reduction defines each case of the proof's case division as a proposition and derives the classification from them. Its 14 declarations, in file order, quoted from CFSG/Assembly/Reduction.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0; each definition is shown whole:

CFSG.Assembly.GroupProp (abbrev, line 10). A definition.

abbrev GroupProp : Type 1 := ∀ (G : Type) [Group G], Prop

CFSG.Assembly.KProper (def, line 14). A definition.

@[expose] def KProper (G : Type) [Group G] : Prop := KCore.KProperNonab C G

CFSG.Assembly.OddOrderStatement (def, line 16). A definition.

@[expose] def OddOrderStatement : Prop :=
  ∀ (G : Type) [Group G] [Finite G], Odd (Nat.card G) → Group.IsSolvable G

CFSG.Assembly.AbelianStatement (def, line 19). A definition.

@[expose] def AbelianStatement : Prop :=
  ∀ (G : Type) [Group G] [Finite G] [IsSimpleGroup G], (∀ a b : G, a * b = b * a) → C G

CFSG.Assembly.DisconnectedStatement (def, line 22). A definition.

@[expose] def DisconnectedStatement : Prop :=
  ∀ (G : Type) [Group G] [Finite G] [IsSimpleGroup G], (∃ a b : G, a * b ≠ b * a) →
    Even (Nat.card G) → ¬ (involutionGraph G).Preconnected → C G

CFSG.Assembly.LowTwoRankStatement (def, line 26). A definition.

@[expose] def LowTwoRankStatement : Prop :=
  ∀ (G : Type) [Group G] [Finite G] [IsSimpleGroup G], (∃ a b : G, a * b ≠ b * a) →
    Even (Nat.card G) → twoRank G ≤ 2 → C G

CFSG.Assembly.DichotomyStatement (def, line 30). A definition.

@[expose] def DichotomyStatement : Prop :=
  ∀ (G : Type) [Group G] [Finite G] [IsSimpleGroup G], (∃ a b : G, a * b ≠ b * a) →
    3 ≤ twoRank G → (involutionGraph G).Connected → IsComponentType G ∨ IsCharTwoType G

CFSG.Assembly.ComponentStatement (def, line 34). A definition.

@[expose] def ComponentStatement : Prop :=
  ∀ (G : Type) [Group G] [Finite G] [IsSimpleGroup G], (∃ a b : G, a * b ≠ b * a) →
    KProper C G → 3 ≤ twoRank G → IsComponentType G → C G

CFSG.Assembly.QuasithinStatement (def, line 38). A definition.

@[expose] def QuasithinStatement : Prop :=
  ∀ (G : Type) [Group G] [Finite G] [IsSimpleGroup G], (∃ a b : G, a * b ≠ b * a) →
    KProper C G → IsCharTwoType G → evenRank G ≤ 2 → C G

CFSG.Assembly.RankThreeStatement (def, line 42). A definition.

@[expose] def RankThreeStatement : Prop :=
  ∀ (G : Type) [Group G] [Finite G] [IsSimpleGroup G], (∃ a b : G, a * b ≠ b * a) →
    KProper C G → IsCharTwoType G → evenRank G = 3 → C G

CFSG.Assembly.LargeEvenStatement (def, line 46). A definition.

@[expose] def LargeEvenStatement : Prop :=
  ∀ (G : Type) [Group G] [Finite G] [IsSimpleGroup G], (∃ a b : G, a * b ≠ b * a) →
    KProper C G → IsCharTwoType G → 4 ≤ evenRank G → C G

CFSG.Assembly.charTwo_classification (theorem, line 50). Proved here.

theorem charTwo_classification (hqt : QuasithinStatement C) (hr3 : RankThreeStatement C)
    (hle : LargeEvenStatement C) (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a) (hK : KProper C G) (hchar : IsCharTwoType G) : C G

CFSG.Assembly.kProper_classification (theorem, line 58). Proved here.

theorem kProper_classification (hodd : OddOrderStatement) (hab : AbelianStatement C)
    (hdisc : DisconnectedStatement C) (hlow : LowTwoRankStatement C) (hdich : DichotomyStatement)
    (hcomp : ComponentStatement C) (hqt : QuasithinStatement C) (hr3 : RankThreeStatement C)
    (hle : LargeEvenStatement C) (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hK : KProper C G) : C G

CFSG.Assembly.classification (theorem, line 81). Proved here.

theorem classification (hodd : OddOrderStatement) (hab : AbelianStatement C)
    (hdisc : DisconnectedStatement C) (hlow : LowTwoRankStatement C) (hdich : DichotomyStatement)
    (hcomp : ComponentStatement C) (hqt : QuasithinStatement C) (hr3 : RankThreeStatement C)
    (hle : LargeEvenStatement C) (G : Type) [Group G] [Finite G] [IsSimpleGroup G] : C G
Sources
LeanCFSG.Assembly.GroupProp · CFSG.Assembly.KProper · CFSG.Assembly.OddOrderStatement · CFSG.Assembly.AbelianStatement · CFSG.Assembly.DisconnectedStatement · CFSG.Assembly.LowTwoRankStatement · CFSG.Assembly.DichotomyStatement · CFSG.Assembly.ComponentStatement · CFSG.Assembly.QuasithinStatement · CFSG.Assembly.RankThreeStatement · CFSG.Assembly.LargeEvenStatement · CFSG.Assembly.charTwo_classification · CFSG.Assembly.kProper_classification · CFSG.Assembly.classification
Used by 1
Used byCFSG.classification_finite_simple_groups

TheoremCFSG.FeitThompson.isSolvable_of_odd_natCard#

The case hodd : OddOrderStatement of CFSG.Assembly.classification. What it asserts, defined in CFSG/Assembly/Reduction.lean, line 16:

@[expose] def OddOrderStatement : Prop :=
  ∀ (G : Type) [Group G] [Finite G], Odd (Nat.card G) → Group.IsSolvable G

The theorem the top theorem's proof gives for it, quoted from CFSG/FeitThompson/OddOrderTheorem.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.FeitThompson.isSolvable_of_odd_natCard (theorem, line 14). Proved here.

theorem isSolvable_of_odd_natCard (G : Type*) [Group G] [Finite G] (hG : Odd (Nat.card G)) :
    Group.IsSolvable G

Its file imports none of the milestone modules, directly or through other files.

Sources
LeanCFSG.FeitThompson.isSolvable_of_odd_natCard
Used by 6
Used byCFSG.classification_finite_simple_groups · CL_LIT_Fischer_three_transposition_theorem · CL_LIT_Timmesfeld_root_involutions · CL_LIT_Walter_abelian_Sylow_two_simple · OO_odd_order_solvable · QT_unique_Shult_simple_strongly_closed_TI_models

TheoremCFSG.Assembly.abelian_simple#

The case hab : AbelianStatement of CFSG.Assembly.classification. What it asserts, defined in CFSG/Assembly/Reduction.lean, line 19:

@[expose] def AbelianStatement : Prop :=
  ∀ (G : Type) [Group G] [Finite G] [IsSimpleGroup G], (∀ a b : G, a * b = b * a) → C G

The theorem the top theorem's proof gives for it, quoted from CFSG/Assembly/InCatalog.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Assembly.abelian_simple (theorem, line 12). Proved here.

theorem abelian_simple (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hcomm : ∀ a b : G, a * b = b * a) : InCatalog G

Its file imports none of the milestone modules, directly or through other files.

Sources
LeanCFSG.Assembly.abelian_simple
Used by 1
Used byCFSG.classification_finite_simple_groups

TheoremCFSG.Assembly.disconnected_involution_graph#

The case hdisc : DisconnectedStatement of CFSG.Assembly.classification. What it asserts, defined in CFSG/Assembly/Reduction.lean, line 22:

@[expose] def DisconnectedStatement : Prop :=
  ∀ (G : Type) [Group G] [Finite G] [IsSimpleGroup G], (∃ a b : G, a * b ≠ b * a) →
    Even (Nat.card G) → ¬ (involutionGraph G).Preconnected → C G

The theorem the top theorem's proof gives for it, quoted from CFSG/Assembly/Disconnected.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Assembly.disconnected_involution_graph (theorem, line 65). Proved here.

theorem disconnected_involution_graph (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a) (heven : Even (Nat.card G))
    (hdisc : ¬ (involutionGraph G).Preconnected) : InCatalog G

Its file imports none of the milestone modules, directly or through other files.

Sources
LeanCFSG.Assembly.disconnected_involution_graph
Used by 7
Used byCFSG.classification_finite_simple_groups · CLS_disconnected_simple_involution_graph_classification · CL_LIT_Aschbacher_proper_two_generated_core · CL_LIT_Gorenstein_Walter_L_balance · CT_even_standard_residual_reduction · QT_faithful_local_empty_classification · QTFE_unique_centralizer_six_model_recognition

TheoremCFSG.Assembly.low_two_rank#

The case hlow : LowTwoRankStatement of CFSG.Assembly.classification. What it asserts, defined in CFSG/Assembly/Reduction.lean, line 26:

@[expose] def LowTwoRankStatement : Prop :=
  ∀ (G : Type) [Group G] [Finite G] [IsSimpleGroup G], (∃ a b : G, a * b ≠ b * a) →
    Even (Nat.card G) → twoRank G ≤ 2 → C G

The theorem the top theorem's proof gives for it, quoted from CFSG/Assembly/LowTwoRank.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Assembly.low_two_rank (theorem, line 51). Proved here.

theorem low_two_rank
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a) (heven : Even (Nat.card G))
    (hrank : twoRank G ≤ 2) : InCatalog G

Its file imports, directly or through other files, 8 milestone modules: CLS_connectivity_MacWilliams_four_generator, FAM_classical_model_membership, LC_GL_local_rank_bounds, LR_Glauberman_Z_star_central_Sylow_involution, LR_dihedral_simple_recognition, LR_rank_two_isomorphism_types, OO_odd_order_solvable, SE_simple_strong_embedding_models.

Sources
LeanCFSG.Assembly.low_two_rank
Uses 2 · Used by 4
Statement usesLC_GL_local_rank_bounds · LR_rank_two_isomorphism_types
Used byCFSG.classification_finite_simple_groups · CL_LIT_Aschbacher_proper_two_generated_core · CLS_low_two_rank_classification · LR_nonabelian_simple_two_rank_lower_bound

TheoremCFSG.Assembly.component_dichotomy#

The case hdich : DichotomyStatement of CFSG.Assembly.classification. What it asserts, defined in CFSG/Assembly/Reduction.lean, line 30:

@[expose] def DichotomyStatement : Prop :=
  ∀ (G : Type) [Group G] [Finite G] [IsSimpleGroup G], (∃ a b : G, a * b ≠ b * a) →
    3 ≤ twoRank G → (involutionGraph G).Connected → IsComponentType G ∨ IsCharTwoType G

The theorem the top theorem's proof gives for it, quoted from CFSG/Assembly/Dichotomy.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Assembly.component_dichotomy (theorem, line 75). Proved here.

theorem component_dichotomy (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a) (hrank : 3 ≤ twoRank G)
    (hconn : (involutionGraph G).Connected) : IsComponentType G ∨ IsCharTwoType G

Its file imports, directly or through other files, 4 milestone modules: CLS_component_free_centralizer_quotient_characteristic_two, CLS_component_free_involution_odd_cores_trivial, CLS_involution_centralizers_characteristic_two_transfer, OO_odd_order_solvable.

Sources
LeanCFSG.Assembly.component_dichotomy
Uses 2 · Used by 2
Statement usesCLS_component_free_involution_odd_cores_trivial · CLS_involution_centralizers_characteristic_two_transfer
Used byCFSG.classification_finite_simple_groups · CLS_component_dichotomy

TheoremCFSG.Assembly.component_type#

The case hcomp : ComponentStatement of CFSG.Assembly.classification. What it asserts, defined in CFSG/Assembly/Reduction.lean, line 34:

@[expose] def ComponentStatement : Prop :=
  ∀ (G : Type) [Group G] [Finite G] [IsSimpleGroup G], (∃ a b : G, a * b ≠ b * a) →
    KProper C G → 3 ≤ twoRank G → IsComponentType G → C G

The theorem the top theorem's proof gives for it, quoted from CFSG/Assembly/ComponentType.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Assembly.component_type (theorem, line 3515). Proved here.

theorem component_type
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a) (hK : KProper InCatalog G) (hrank : 3 ≤ twoRank G)
    (hcomp : IsComponentType G) : InCatalog G

Its file imports, directly or through other files, 59 milestone modules: AT_alternating_automorphism_permutation, CLS_component_dichotomy, CLS_component_free_centralizer_quotient_characteristic_two, CLS_component_free_involution_odd_cores_trivial, CLS_connectivity_MacWilliams_four_generator, CLS_involution_centralizers_characteristic_two_transfer, CL_LIT_Aschbacher_component_type_theorem_5, CL_LIT_Aschbacher_proper_two_generated_core, CL_LIT_Borel_Tits_local_parabolic, CL_LIT_Curtis_Tits_presentation_theorem, CL_LIT_Fischer_3T_existence_uniqueness, CL_LIT_Fischer_three_transposition_theorem, CL_LIT_GH74_sectional_two_rank_four, CL_LIT_GMS_Monster_uniqueness, CL_LIT_Goldschmidt_strongly_closed_abelian, CL_LIT_Goldschmidt_strongly_closed_abelian_models, CL_LIT_Gorenstein_Walter_L_balance, CL_LIT_Griess_Schur_multipliers_Lie_type, CL_LIT_Monster_existence_Griess_Conway, CL_LIT_SQTK_simple_list, CL_LIT_SQTK_simple_listBase, CL_LIT_Stroth_Leon_Sims_Baby_Monster_recognition, CL_LIT_Walter_abelian_Sylow_two_simple, CL_LIT_classical_involution_theorem, CL_LIT_signalizer_functor_theorem, CTB_KProper_component_local_B, CTGMS_Bender_1971_even_rank_one_model_and_strong_embedding_input, CTSS_sporadic_standard_centerless_M12_J2_and_other_quotients_frontier, CTU_KProper_simple_unbalanced_recognition, CT_Seitz_centerless_reduction_frontier, CT_catalog_nonabelian_type_partition, CT_even_small_Lie_standard_frontier, CT_even_standard_residual_reduction, CT_initial_standard_component_frontier, CT_odd_standard_recognition_frontier, CT_quaternion_component_recognition_frontier, CT_rank_two_standard_recognition_frontier, CT_standard_recognition_assembly, FAM_M_finiteness, FAM_M_simplicity, FAM_Th_simplicity, FAM_classical_model_membership, FAM_sporadic_converse, LC_GL_local_rank_bounds, LC_generalized_fitting_self_centralizing, LR_Brauer_Suzuki_central_involution, LR_Glauberman_Z_star_central_Sylow_involution, LR_dihedral_simple_recognition, LR_nonabelian_simple_two_rank_lower_bound, LR_rank_two_isomorphism_types, LR_semidihedral_simple_recognition, LR_wreathed_simple_recognition, OO_odd_order_solvable, QT_faithful_local_empty_classification, QT_unique_Shult_simple_strongly_closed_TI_models, QT_unique_maximal_local_classification, SE_simple_strong_embedding_models, SG_two_signalizer_completeness, ZJ_glauberman_characteristic.

Sources
LeanCFSG.Assembly.component_type
Uses 3 · Used by 4
Statement usesCTB_KProper_component_local_B · CT_quaternion_component_recognition_frontier · CT_standard_recognition_assembly
Used byCFSG.classification_finite_simple_groups · CLS_component_classification · CL_LIT_GL83_Theorem_C_preuniqueness_rank_three · R3E_part_two_prime_three_outcome

TheoremCFSG.Assembly.quasithin#

The case hqt : QuasithinStatement of CFSG.Assembly.classification. What it asserts, defined in CFSG/Assembly/Reduction.lean, line 38:

@[expose] def QuasithinStatement : Prop :=
  ∀ (G : Type) [Group G] [Finite G] [IsSimpleGroup G], (∃ a b : G, a * b ≠ b * a) →
    KProper C G → IsCharTwoType G → evenRank G ≤ 2 → C G

The theorem the top theorem's proof gives for it, quoted from CFSG/Assembly/Quasithin.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Assembly.quasithin (theorem, line 1875). Proved here.

theorem quasithin
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a) (hK : KProper InCatalog G) (hchar : IsCharTwoType G)
    (he : evenRank G ≤ 2) : InCatalog G

Its file imports, directly or through other files, 43 milestone modules: AT_alternating_automorphism_permutation, CLS_component_dichotomy, CLS_component_free_centralizer_quotient_characteristic_two, CLS_component_free_involution_odd_cores_trivial, CLS_connectivity_MacWilliams_four_generator, CLS_involution_centralizers_characteristic_two_transfer, CL_LIT_Borel_Tits_local_parabolic, CL_LIT_Curtis_Tits_presentation_theorem, CL_LIT_Fischer_3T_existence_uniqueness, CL_LIT_Fischer_three_transposition_theorem, CL_LIT_GMS_Monster_uniqueness, CL_LIT_Goldschmidt_strongly_closed_abelian, CL_LIT_Goldschmidt_strongly_closed_abelian_models, CL_LIT_Gorenstein_Walter_L_balance, CL_LIT_Griess_Schur_multipliers_Lie_type, CL_LIT_Monster_existence_Griess_Conway, CL_LIT_SQTK_simple_list, CL_LIT_SQTK_simple_listBase, CL_LIT_Stroth_Leon_Sims_Baby_Monster_recognition, CL_LIT_Walter_abelian_Sylow_two_simple, CL_LIT_signalizer_functor_theorem, CTGMS_Bender_1971_even_rank_one_model_and_strong_embedding_input, CT_catalog_nonabelian_type_partition, FAM_M_finiteness, FAM_M_simplicity, FAM_Th_simplicity, FAM_classical_model_membership, LC_GL_local_rank_bounds, LC_generalized_fitting_self_centralizing, LR_Brauer_Suzuki_central_involution, LR_Glauberman_Z_star_central_Sylow_involution, LR_dihedral_simple_recognition, LR_nonabelian_simple_two_rank_lower_bound, LR_rank_two_isomorphism_types, LR_semidihedral_simple_recognition, LR_wreathed_simple_recognition, OO_odd_order_solvable, QT_H13_maximal_local_catalog_assembly, QT_faithful_local_empty_classification, QT_faithful_local_nonempty_classification, QT_unique_Shult_simple_strongly_closed_TI_models, QT_unique_maximal_local_classification, SE_simple_strong_embedding_models.

Sources
LeanCFSG.Assembly.quasithin
Uses 2 · Used by 3
Statement usesQT_faithful_local_nonempty_classification · QT_unique_maximal_local_classification
Used byCFSG.classification_finite_simple_groups · CLS_characteristic_two_classification · CLS_K_proper_simple_classification

TheoremCFSG.Assembly.rank_three_even#

The case hr3 : RankThreeStatement of CFSG.Assembly.classification. What it asserts, defined in CFSG/Assembly/Reduction.lean, line 42:

@[expose] def RankThreeStatement : Prop :=
  ∀ (G : Type) [Group G] [Finite G] [IsSimpleGroup G], (∃ a b : G, a * b ≠ b * a) →
    KProper C G → IsCharTwoType G → evenRank G = 3 → C G

The theorem the top theorem's proof gives for it, quoted from CFSG/Assembly/RankThreeEven.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Assembly.rank_three_even (theorem, line 3712). Proved here.

theorem rank_three_even
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a) (hK : KProper InCatalog G) (hchar : IsCharTwoType G)
    (he : evenRank G = 3) : InCatalog G

Its file imports, directly or through other files, 70 milestone modules: AT_alternating_automorphism_permutation, CAT_native_realization, CLS_component_dichotomy, CLS_component_free_centralizer_quotient_characteristic_two, CLS_component_free_involution_odd_cores_trivial, CLS_connectivity_MacWilliams_four_generator, CLS_involution_centralizers_characteristic_two_transfer, CLS_low_two_rank_classification, CL_LIT_AS_vol_I_background, CL_LIT_Aschbacher_1983_uniqueness_case_rank_three, CL_LIT_Aschbacher_component_type_theorem_5, CL_LIT_Aschbacher_proper_two_generated_core, CL_LIT_Borel_Tits_local_parabolic, CL_LIT_Curtis_Tits_presentation_theorem, CL_LIT_Fischer_3T_existence_uniqueness, CL_LIT_Fischer_three_transposition_theorem, CL_LIT_GH74_sectional_two_rank_four, CL_LIT_GL83_Theorem_C_preuniqueness_rank_three, CL_LIT_GMS_Monster_uniqueness, CL_LIT_Goldschmidt_strongly_closed_abelian, CL_LIT_Goldschmidt_strongly_closed_abelian_models, CL_LIT_Gorenstein_Walter_L_balance, CL_LIT_Griess_Schur_multipliers_Lie_type, CL_LIT_Monster_existence_Griess_Conway, CL_LIT_SQTK_simple_list, CL_LIT_SQTK_simple_listBase, CL_LIT_Stroth_Leon_Sims_Baby_Monster_recognition, CL_LIT_Timmesfeld_1978_large_extraspecial, CL_LIT_Walter_abelian_Sylow_two_simple, CL_LIT_classical_involution_theorem, CL_LIT_signalizer_functor_theorem, CTB_KProper_component_local_B, CTGMS_Bender_1971_even_rank_one_model_and_strong_embedding_input, CTSS_sporadic_standard_centerless_M12_J2_and_other_quotients_frontier, CTU_KProper_simple_unbalanced_recognition, CT_Seitz_centerless_reduction_frontier, CT_catalog_nonabelian_type_partition, CT_even_small_Lie_standard_frontier, CT_even_standard_residual_reduction, CT_initial_standard_component_frontier, CT_odd_standard_recognition_frontier, CT_quaternion_component_recognition_frontier, CT_rank_two_standard_recognition_frontier, CT_standard_recognition_assembly, FAM_M_finiteness, FAM_M_simplicity, FAM_Th_simplicity, FAM_classical_model_membership, FAM_sporadic_converse, LC_GL_embedding_theorem_D1_rank_four, LC_GL_embedding_theorem_D2_rank_four, LC_GL_local_rank_bounds, LC_generalized_fitting_self_centralizing, LR_Brauer_Suzuki_central_involution, LR_Glauberman_Z_star_central_Sylow_involution, LR_dihedral_simple_recognition, LR_nonabelian_simple_two_rank_lower_bound, LR_rank_two_isomorphism_types, LR_semidihedral_simple_recognition, LR_wreathed_simple_recognition, OO_odd_order_solvable, QT_faithful_local_empty_classification, QT_unique_Shult_simple_strongly_closed_TI_models, QT_unique_maximal_local_classification, R3E_part_one_outcome_assembly, R3E_part_two_prime_three_outcome, R3E_rank_three_core_uniqueness_exclusion, SE_simple_strong_embedding_models, SG_two_signalizer_completeness, ZJ_glauberman_characteristic.

Sources
LeanCFSG.Assembly.rank_three_even
Uses 3 · Used by 4
Statement usesR3E_part_one_outcome_assembly · R3E_part_two_prime_three_outcome · R3E_rank_three_core_uniqueness_exclusion
Used byCFSG.classification_finite_simple_groups · CLS_characteristic_two_classification · CLS_K_proper_simple_classification · CLS_rank_three_even_classification

TheoremCFSG.Assembly.large_even#

The case hle : LargeEvenStatement of CFSG.Assembly.classification. What it asserts, defined in CFSG/Assembly/Reduction.lean, line 46:

@[expose] def LargeEvenStatement : Prop :=
  ∀ (G : Type) [Group G] [Finite G] [IsSimpleGroup G], (∃ a b : G, a * b ≠ b * a) →
    KProper C G → IsCharTwoType G → 4 ≤ evenRank G → C G

The theorem the top theorem's proof gives for it, quoted from CFSG/Assembly/LargeEven.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Assembly.large_even (theorem, line 3740). Proved here.

theorem large_even
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a) (hK : KProper InCatalog G) (hchar : IsCharTwoType G)
    (he : 4 ≤ evenRank G) : InCatalog G

Its file imports, directly or through other files, 59 milestone modules: AT_alternating_automorphism_permutation, CAT_native_realization, CLS_component_dichotomy, CLS_component_free_centralizer_quotient_characteristic_two, CLS_component_free_involution_odd_cores_trivial, CLS_connectivity_MacWilliams_four_generator, CLS_involution_centralizers_characteristic_two_transfer, CL_LIT_Aschbacher_component_type_theorem_5, CL_LIT_Aschbacher_proper_two_generated_core, CL_LIT_Borel_Tits_local_parabolic, CL_LIT_Curtis_Tits_presentation_theorem, CL_LIT_Fischer_3T_existence_uniqueness, CL_LIT_Fischer_three_transposition_theorem, CL_LIT_GH74_sectional_two_rank_four, CL_LIT_GMS_Monster_uniqueness, CL_LIT_Goldschmidt_strongly_closed_abelian, CL_LIT_Goldschmidt_strongly_closed_abelian_models, CL_LIT_Gorenstein_Walter_L_balance, CL_LIT_Griess_Schur_multipliers_Lie_type, CL_LIT_Monster_existence_Griess_Conway, CL_LIT_SQTK_simple_list, CL_LIT_SQTK_simple_listBase, CL_LIT_Stroth_Leon_Sims_Baby_Monster_recognition, CL_LIT_Timmesfeld_1978_large_extraspecial, CL_LIT_Walter_abelian_Sylow_two_simple, CL_LIT_classical_involution_theorem, CL_LIT_signalizer_functor_theorem, CTGMS_Bender_1971_even_rank_one_model_and_strong_embedding_input, CT_catalog_nonabelian_type_partition, FAM_M_finiteness, FAM_M_simplicity, FAM_Th_simplicity, FAM_classical_model_membership, FAM_sporadic_converse, LC_GL_GF2_recognition_rank_four, LC_GL_constructed_pretrichotomy_rank_four, LC_GL_embedding_theorem_D1_rank_four, LC_GL_embedding_theorem_D2_rank_four, LC_GL_local_rank_bounds, LC_GL_preuniqueness_exclusion_rank_four, LC_GL_standard_type_recognition_rank_four, LC_GL_theorem_A, LC_GL_theorem_C_rank_four, LC_GL_uniqueness_exclusion_rank_four, LC_generalized_fitting_self_centralizing, LR_Brauer_Suzuki_central_involution, LR_Glauberman_Z_star_central_Sylow_involution, LR_dihedral_simple_recognition, LR_nonabelian_simple_two_rank_lower_bound, LR_rank_two_isomorphism_types, LR_semidihedral_simple_recognition, LR_wreathed_simple_recognition, OO_odd_order_solvable, QT_faithful_local_empty_classification, QT_unique_Shult_simple_strongly_closed_TI_models, QT_unique_maximal_local_classification, SE_simple_strong_embedding_models, SG_two_signalizer_completeness, ZJ_glauberman_characteristic.

Sources
LeanCFSG.Assembly.large_even
Uses 4 · Used by 4
Statement usesLC_GL_GF2_recognition_rank_four · LC_GL_constructed_pretrichotomy_rank_four · LC_GL_preuniqueness_exclusion_rank_four · LC_GL_standard_type_recognition_rank_four
Used byCFSG.classification_finite_simple_groups · CLS_characteristic_two_classification · CLS_K_proper_simple_classification · CLS_large_even_classification

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.