Milestones
The 110 modules directly under CFSG/Milestones/, by file name, one article each; CFSG/Milestones.lean imports 108 of them. 31 milestones are imported by no case theorem's file, directly or through other files.
AT_alternating_automorphism_perm… to CLS_large_even_classification
- AT_alternating_automorphism_permutation
- BI_Brauer_characterization
- BL_block_section_column_orthogonality
- BT_principal_block_Brauer_correspondence
- CAT_converse
- CAT_native_realization
- CFSG_classification
- CFSG_exhaustiveness
- CLS_K_proper_simple_classification
- CLS_QTKE_classification
- CLS_abelian_simple_catalog
- CLS_characteristic_two_classification
- CLS_component_classification
- CLS_component_dichotomy
- CLS_component_free_centralizer_quotient_characteristic_two
- CLS_component_free_involution_odd_cores_trivial
- CLS_connectivity_MacWilliams_four_generator
- CLS_disconnected_simple_involution_graph_classification
- CLS_involution_centralizers_characteristic_two_transfer
- CLS_large_even_classification
CLS_low_two_rank_classification to CL_LIT_SQTK_simple_list
- CLS_low_two_rank_classification
- CLS_rank_three_even_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_Gilman_Solomon_maximal_unbalancing_reduction
- 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 to CT_rank_two_standard_recognition…
- CL_LIT_SQTK_simple_listBase
- CL_LIT_Steinberg_presentation_theorem
- CL_LIT_Stroth_Leon_Sims_Baby_Monster_recognition
- CL_LIT_Timmesfeld_1978_large_extraspecial
- CL_LIT_Timmesfeld_root_involutions
- 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 to LC_GL_embedding_theorem_D2_rank_…
- CT_standard_recognition_assembly
- FAM_M_finiteness
- FAM_M_simplicity
- FAM_Th_simplicity
- FAM_classical_model_membership
- FAM_sporadic_converse
- FAM_sporadic_finiteness
- FAM_sporadic_native_converse
- FAM_sporadic_representatives
- FROB_kernel_existence
- GW_original_maximal_odd_S_invariant_R_and_normalizer_core
- GW_original_normalizer_R_pure_projective_shared_fourgroup_and_index_divisor
- GW_original_normalizer_coset_involution_fixedpoints_secondary_torus_divisibility
- GW_original_post_proposition_sixteen_all_prime_stationarity_and_no_growth
- GW_original_post_proposition_sixteen_canonical_stationary_prime_normalizers
- GW_original_q_five_index_three_character_kernel_order_contradiction
- 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 to QT_primitive_regular_cyclic_Burn…
- 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
- QTFE_unique_centralizer_six_model_recognition
- QT_H13_maximal_local_catalog_assembly
- QT_faithful_local_empty_classification
- QT_faithful_local_nonempty_classification
- QT_primitive_regular_cyclic_Burnside_Schur
QT_unique_Shult_simple_strongly_… to ZJ_glauberman_replacement
- QT_unique_Shult_simple_strongly_closed_TI_models
- QT_unique_maximal_local_classification
- R3E_model_outcomes_catalog
- 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
- ZJ_glauberman_replacement
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.