LC_GL_local_rank_bounds to QT_primitive_regular_cyclic_Burn…

TheoremLC_GL_local_rank_bounds#

The milestone module CFSG.Milestones.LC_GL_local_rank_bounds, one of those CFSG/Milestones.lean imports.

It declares 1 result, quoted from CFSG/Milestones/LC_GL_local_rank_bounds.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Milestones.lc_gl_local_rank_bounds (theorem, line 14). Proved here.

theorem _root_.CFSG.Milestones.lc_gl_local_rank_bounds (X : Type*) [Group X] [Finite X] :
    (∀ p : ℕ, p.Prime → p ≠ 2 →
      localRank p X ≤ pRank p (⊤ : Subgroup X) ∧ localRank p X ≤ evenRank X) ∧
    (∀ k : ℕ, 1 ≤ k → ((oddStrata k X).Nonempty ↔ k ≤ evenRank X)) ∧
    oddStrata (evenRank X + 1) X = ∅ ∧
    ∀ k : ℕ, 1 ≤ k → oddStrata (k + 1) X ⊆ oddStrata k X

The files of 5 case theorems import it, directly or through other files: CFSG.Assembly.low_two_rank, CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.

Sources
LeanCFSG.Milestones.lc_gl_local_rank_bounds
Used by 5
Used byCFSG.Assembly.low_two_rank · CL_LIT_Griess_Schur_multipliers_Lie_type · CL_LIT_signalizer_functor_theorem · CT_even_small_Lie_standard_frontier · CT_initial_standard_component_frontier

TheoremLC_GL_preuniqueness_exclusion_rank_four#

The milestone module CFSG.Milestones.LC_GL_preuniqueness_exclusion_rank_four, one of those CFSG/Milestones.lean imports.

It declares 1 result, quoted from CFSG/Milestones/LC_GL_preuniqueness_exclusion_rank_four.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Milestones.lc_gl_preuniqueness_exclusion_rank_four (theorem, line 3307). Proved here.

theorem _root_.CFSG.Milestones.lc_gl_preuniqueness_exclusion_rank_four
    (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) :
    ∃ p ∈ LargeEvenBeta 4 G, ¬ LargeEvenWeakCoreLocal G p

The files of 1 case theorem import it, directly or through other files: CFSG.Assembly.large_even.

Sources
LeanCFSG.Milestones.lc_gl_preuniqueness_exclusion_rank_four
Uses 2 · Used by 1
Statement usesLC_GL_theorem_C_rank_four · LC_GL_uniqueness_exclusion_rank_four
Used byCFSG.Assembly.large_even

TheoremLC_GL_standard_type_recognition_rank_four#

The milestone module CFSG.Milestones.LC_GL_standard_type_recognition_rank_four, one of those CFSG/Milestones.lean imports.

It declares 2 results, quoted from CFSG/Milestones/LC_GL_standard_type_recognition_rank_four.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Milestones.lc_gl_standard_type_lie_char_two_recognition_rank_four (theorem, line 240). Proved here.

theorem _root_.CFSG.Milestones.lc_gl_standard_type_lie_char_two_recognition_rank_four
    (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) (p : ℕ) (hp : p ∈ LargeEvenBeta 4 G) (B : Subgroup G) (x : G)
    (L : Subgroup G) (hS : LargeEvenSStar p B x L) (hst : LargeEvenStandardType p B x L) :
    InLieTypeCharTwoCatalog G

CFSG.Milestones.lc_gl_standard_type_recognition_rank_four (theorem, line 264). Proved here.

theorem _root_.CFSG.Milestones.lc_gl_standard_type_recognition_rank_four
    (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) (p : ℕ) (hp : p ∈ LargeEvenBeta 4 G) (B : Subgroup G) (x : G)
    (L : Subgroup G) (hS : LargeEvenSStar p B x L) (hst : LargeEvenStandardType p B x L) :
    InCatalog G

The files of 1 case theorem import it, directly or through other files: CFSG.Assembly.large_even.

Sources
LeanCFSG.Milestones.lc_gl_standard_type_lie_char_two_recognition_rank_four · CFSG.Milestones.lc_gl_standard_type_recognition_rank_four
Uses 4 · Used by 1
Statement usesCAT_native_realization · CL_LIT_GH74_sectional_two_rank_four · CL_LIT_Gorenstein_Walter_L_balance · FAM_sporadic_converse
Used byCFSG.Assembly.large_even

TheoremLC_GL_theorem_A#

The milestone module CFSG.Milestones.LC_GL_theorem_A, one of those CFSG/Milestones.lean imports.

It declares 1 result, quoted from CFSG/Milestones/LC_GL_theorem_A.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Milestones.lc_gl_theorem_a (theorem, line 1757). Proved here.

theorem _root_.CFSG.Milestones.lc_gl_theorem_a
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a)
    (hK : IsKProper G) (hchar : IsCharTwoType G) (he : 4 ≤ evenRank G)
    (m : ℕ) (hm : 4 ≤ m)
    (ha : ∀ q ∈ GLABeta (m + 1) G, GLAWeakCoreLocal G q)
    (hb : ∀ q ∈ GLABeta m G, GLAWeakCoreLocal G q ∨ GLADeltaZero G q)
    (hc : ∃ q ∈ GLABeta m G, GLATwoLocalRank q G = m ∧ GLADeltaZero G q) :
    ∃ p ∈ GLABeta m G, GLATwoLocalRank p G = m ∧ GLADeltaZero G p ∧
      ((p = 3 ∧ GLAGF2Type G) ∨
        ∃ (B : Subgroup G) (x : G) (L : Subgroup G),
          GLASStar p B x L ∧ GLAStandardType p B x L)

The files of 1 case theorem import it, directly or through other files: CFSG.Assembly.large_even.

Sources
LeanCFSG.Milestones.lc_gl_theorem_a
Uses 4 · Used by 1
Statement usesCAT_native_realization · CL_LIT_Gorenstein_Walter_L_balance · CL_LIT_Timmesfeld_1978_large_extraspecial · FAM_sporadic_converse
Used byLC_GL_constructed_pretrichotomy_rank_four

TheoremLC_GL_theorem_C_rank_four#

The milestone module CFSG.Milestones.LC_GL_theorem_C_rank_four, one of those CFSG/Milestones.lean imports.

It declares 1 result, quoted from CFSG/Milestones/LC_GL_theorem_C_rank_four.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Milestones.lc_gl_theorem_c_rank_four (theorem, line 2621). Proved here.

theorem _root_.CFSG.Milestones.lc_gl_theorem_c_rank_four
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a)
    (hK : IsKProper G) (hchar : IsCharTwoType G) (he : 4 ≤ evenRank G)
    (hpre : GLBPreuniqueness G) :
    GLBUniqueFour G

The files of 1 case theorem import it, directly or through other files: CFSG.Assembly.large_even.

Sources
LeanCFSG.Milestones.lc_gl_theorem_c_rank_four
Uses 3 · Used by 1
Statement usesCAT_native_realization · FAM_sporadic_converse · LC_GL_embedding_theorem_D2_rank_four
Used byLC_GL_preuniqueness_exclusion_rank_four

TheoremLC_GL_uniqueness_exclusion_rank_four#

The milestone module CFSG.Milestones.LC_GL_uniqueness_exclusion_rank_four, one of those CFSG/Milestones.lean imports.

It declares 1 result, quoted from CFSG/Milestones/LC_GL_uniqueness_exclusion_rank_four.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Milestones.lc_gl_uniqueness_exclusion_rank_four (theorem, line 3186). Proved here.

theorem _root_.CFSG.Milestones.lc_gl_uniqueness_exclusion_rank_four
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a)
    (hK : IsKProper G) (hchar : IsCharTwoType G) (he : 4 ≤ evenRank G) :
    ¬ uniqueFourUnique G

The files of 1 case theorem import it, directly or through other files: CFSG.Assembly.large_even.

Sources
LeanCFSG.Milestones.lc_gl_uniqueness_exclusion_rank_four
Uses 5 · Used by 1
Statement usesCAT_native_realization · CL_LIT_Gorenstein_Walter_L_balance · CL_LIT_Timmesfeld_1978_large_extraspecial · CL_LIT_classical_involution_theorem · FAM_sporadic_converse
Used byLC_GL_preuniqueness_exclusion_rank_four

TheoremLC_generalized_fitting_self_centralizing#

The milestone module CFSG.Milestones.LC_generalized_fitting_self_centralizing, one of those CFSG/Milestones.lean imports.

It declares 2 results, quoted from CFSG/Milestones/LC_generalized_fitting_self_centralizing.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Milestones.lc_generalized_fitting_self_centralizing (theorem, line 11). Proved here.

theorem lc_generalized_fitting_self_centralizing (G : Type u) [Group G] [Finite G] :
    Subgroup.centralizer
      (CFSG.GorensteinWalter.generalizedFittingSubgroupOf (⊤ : Subgroup G) : Set G) ≤
      CFSG.GorensteinWalter.generalizedFittingSubgroupOf (⊤ : Subgroup G)

CFSG.Milestones.lc_generalized_fitting_self_centralizing_stated (theorem, line 22). Proved here.

theorem _root_.CFSG.Milestones.lc_generalized_fitting_self_centralizing_stated
    (G : Type) [Group G] [Finite G] :
    Subgroup.centralizer (genFittingFStar G : Set G) ≤ genFittingFStar G

The files of 4 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.

Sources
LeanCFSG.Milestones.lc_generalized_fitting_self_centralizing · CFSG.Milestones.lc_generalized_fitting_self_centralizing_stated
Used by 2
Used byCL_LIT_GH74_sectional_two_rank_four · CL_LIT_Gorenstein_Walter_L_balance

TheoremLR_Brauer_Suzuki_central_involution#

The milestone module CFSG.Milestones.LR_Brauer_Suzuki_central_involution, one of those CFSG/Milestones.lean imports.

It declares 2 results, quoted from CFSG/Milestones/LR_Brauer_Suzuki_central_involution.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Milestones.brauer_suzuki (theorem, line 12). Proved here.

theorem _root_.CFSG.Milestones.brauer_suzuki {G : Type*} [Group G] [Finite G]
    (n : ℕ) (hn : 3 ≤ n)
    (P : Sylow 2 G)
    (hquat : Nonempty ((P : Subgroup G) ≃* QuaternionGroup (2 ^ (n - 2))))
    (t : G) (ht_mem : t ∈ (P : Subgroup G)) (ht_ord : orderOf t = 2) :
    (QuotientGroup.mk t : G ⧸ oddCore G) ∈
      Subgroup.center (G ⧸ oddCore G)

CFSG.Milestones.brauer_suzuki_central_involution (theorem, line 26). Proved here.

theorem _root_.CFSG.Milestones.brauer_suzuki_central_involution {G : Type*} [Group G] [Finite G]
    (n : ℕ) (hn : 3 ≤ n)
    (P : Sylow 2 G)
    (hquat : Nonempty ((P : Subgroup G) ≃* QuaternionGroup (2 ^ (n - 2))))
    (t : G) (ht_mem : t ∈ (P : Subgroup G)) (ht_ord : orderOf t = 2) :
    (QuotientGroup.mk t : G ⧸ oddCore G) ≠ 1 ∧
      (QuotientGroup.mk t : G ⧸ oddCore G) ∈ Subgroup.center (G ⧸ oddCore G)

The files of 4 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.

Sources
LeanCFSG.Milestones.brauer_suzuki · CFSG.Milestones.brauer_suzuki_central_involution
Used by 3
Used byCT_even_standard_residual_reduction · QT_faithful_local_empty_classification · QTFE_unique_centralizer_six_model_recognition

TheoremLR_Glauberman_Z_star_central_Sylow_involution#

The milestone module CFSG.Milestones.LR_Glauberman_Z_star_central_Sylow_involution, one of those CFSG/Milestones.lean imports.

It declares 2 results, quoted from CFSG/Milestones/LR_Glauberman_Z_star_central_Sylow_involution.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Milestones.glauberman_zStar (theorem, line 11). Proved here.

theorem _root_.CFSG.Milestones.glauberman_zStar (G : Type) [Group G] [Fintype G]
    (t : G) (ht1 : t ≠ 1) (ht2 : t * t = 1)
    (hisolated : ∀ g : G, (g * t * g⁻¹) * t = t * (g * t * g⁻¹) →
      g * t * g⁻¹ = t) :
    ∃ N : Subgroup G, N.Normal ∧ Odd (Nat.card N) ∧
      ∀ g : G, g * t * g⁻¹ * t⁻¹ ∈ N

CFSG.Milestones.glauberman_zStar_central_sylow_involution (theorem, line 24). Proved here.

theorem _root_.CFSG.Milestones.glauberman_zStar_central_sylow_involution {G : Type} [Group G] [Finite G] (S : Sylow 2 G)
    (z : (S : Subgroup G)) (hzZ : z ∈ Subgroup.center (S : Subgroup G)) (hz : orderOf z = 2)
    (hwc : ∀ g : G, g⁻¹ * (z : G) * g ∈ (S : Subgroup G) → g⁻¹ * (z : G) * g = z) :
    (∀ g : G, ∃ c ∈ Subgroup.centralizer ({(z : G)} : Set G), ∃ k ∈ oddCore G, g = c * k) ∧
      (QuotientGroup.mk (z : G) : G ⧸ oddCore G) ∈ Subgroup.center (G ⧸ oddCore G)

The files of 5 case theorems import it, directly or through other files: CFSG.Assembly.low_two_rank, CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.

Sources
LeanCFSG.Milestones.glauberman_zStar · CFSG.Milestones.glauberman_zStar_central_sylow_involution
Used by 7
Used byCL_LIT_signalizer_functor_theorem · CL_LIT_Timmesfeld_root_involutions · CL_LIT_Walter_abelian_Sylow_two_simple · LR_rank_two_isomorphism_types · LR_semidihedral_simple_recognition · LR_wreathed_simple_recognition · QT_unique_Shult_simple_strongly_closed_TI_models

TheoremLR_dihedral_simple_recognition#

The milestone module CFSG.Milestones.LR_dihedral_simple_recognition, one of those CFSG/Milestones.lean imports.

It declares 1 result, quoted from CFSG/Milestones/LR_dihedral_simple_recognition.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Milestones.lr_dihedral_simple_recognition (theorem, line 13). Proved here.

theorem _root_.CFSG.Milestones.lr_dihedral_simple_recognition (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a) (S : Sylow 2 G) (n : ℕ) (hn : 2 ≤ n)
    (hS : Nonempty ((S : Subgroup G) ≃* DihedralGroup (2 ^ (n - 1)))) :
    (∃ p f : ℕ, p.Prime ∧ p ≠ 2 ∧ 1 ≤ f ∧ LowTwoRank.StatedClassicalModel G .PSL 2 p f) ∨
      Nonempty (G ≃* alternatingGroup (Fin 7))

The files of 5 case theorems import it, directly or through other files: CFSG.Assembly.low_two_rank, CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.

Sources
LeanCFSG.Milestones.lr_dihedral_simple_recognition
Used by 3
Used byLR_rank_two_isomorphism_types · LR_semidihedral_simple_recognition · LR_wreathed_simple_recognition

TheoremLR_nonabelian_simple_two_rank_lower_bound#

The milestone module CFSG.Milestones.LR_nonabelian_simple_two_rank_lower_bound, one of those CFSG/Milestones.lean imports.

It declares 1 result, quoted from CFSG/Milestones/LR_nonabelian_simple_two_rank_lower_bound.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Milestones.lr_nonabelian_simple_two_rank_lower_bound (theorem, line 12). Proved here.

theorem _root_.CFSG.Milestones.lr_nonabelian_simple_two_rank_lower_bound (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a) (heven : Even (Nat.card G)) :
    2 ≤ twoRank G

The files of 4 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.

Sources
LeanCFSG.Milestones.lr_nonabelian_simple_two_rank_lower_bound
Uses 1 · Used by 6
Statement usesCFSG.Assembly.low_two_rank
Used byCL_LIT_Gorenstein_Walter_L_balance · CT_rank_two_standard_recognition_frontier · CT_Seitz_centerless_reduction_frontier · QT_faithful_local_empty_classification · QTFE_unique_centralizer_six_model_recognition · QT_unique_maximal_local_classification

TheoremLR_rank_two_isomorphism_types#

The milestone module CFSG.Milestones.LR_rank_two_isomorphism_types, one of those CFSG/Milestones.lean imports.

It declares 1 result, quoted from CFSG/Milestones/LR_rank_two_isomorphism_types.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Milestones.lr_rank_two_isomorphism_types (theorem, line 13). Proved here.

theorem _root_.CFSG.Milestones.lr_rank_two_isomorphism_types
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a) (hrank : twoRank G = 2) :
    (∃ p f : ℕ, p.Prime ∧ p ≠ 2 ∧ 1 ≤ f ∧ StatedClassicalModel G .PSL 2 p f) ∨
    (∃ p f : ℕ, p.Prime ∧ p ≠ 2 ∧ 1 ≤ f ∧ StatedClassicalModel G .PSL 3 p f) ∨
    (∃ p f : ℕ, p.Prime ∧ p ≠ 2 ∧ 1 ≤ f ∧ StatedClassicalModel G .PSU 3 p f) ∨
    StatedClassicalModel G .PSU 3 2 2 ∨
    Nonempty (G ≃* alternatingGroup (Fin 7)) ∨
    Nonempty (G ≃* StatedM11)

The files of 5 case theorems import it, directly or through other files: CFSG.Assembly.low_two_rank, CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.

Sources
LeanCFSG.Milestones.lr_rank_two_isomorphism_types
Uses 6 · Used by 4
Statement usesCLS_connectivity_MacWilliams_four_generator · FAM_classical_model_membership · LR_Glauberman_Z_star_central_Sylow_involution · LR_dihedral_simple_recognition · OO_odd_order_solvable · SE_simple_strong_embedding_models
Used byCFSG.Assembly.low_two_rank · CL_LIT_Aschbacher_component_type_theorem_5 · CL_LIT_Goldschmidt_strongly_closed_abelian · CL_LIT_Goldschmidt_strongly_closed_abelian_models

TheoremLR_semidihedral_simple_recognition#

The milestone module CFSG.Milestones.LR_semidihedral_simple_recognition, one of those CFSG/Milestones.lean imports.

It declares 2 results, quoted from CFSG/Milestones/LR_semidihedral_simple_recognition.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Milestones.lr_semidihedral_simple_recognition_1 (theorem, line 60). Proved here.

theorem _root_.CFSG.Milestones.lr_semidihedral_simple_recognition_1
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a)
    (hsd : ∃ (S : Sylow 2 G) (n : ℕ), 4 ≤ n ∧
      Nonempty ((S : Subgroup G) ≃* SemidihedralGroup n)) :
    (∃ p f : ℕ, p.Prime ∧ p ≠ 2 ∧ 1 ≤ f ∧ p ^ f % 4 = 3 ∧
        StatedClassicalModel G .PSL 3 p f) ∨
    (∃ p f : ℕ, p.Prime ∧ p ≠ 2 ∧ 1 ≤ f ∧ p ^ f % 4 = 1 ∧
        StatedClassicalModel G .PSU 3 p f) ∨
    Nonempty (G ≃* StatedM11)

CFSG.Milestones.lr_semidihedral_simple_recognition_2 (theorem, line 78). Proved here.

theorem _root_.CFSG.Milestones.lr_semidihedral_simple_recognition_2
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a)
    (P : Sylow 2 G)
    (hsd : ∃ n : ℕ, 4 ≤ n ∧ Nonempty ((P : Subgroup G) ≃* SemidihedralGroup n)) :
    (∃ p k : ℕ, ∃ _hp : Fact p.Prime, 0 < k ∧ p ^ k % 4 = 3 ∧
        Nonempty (G ≃* PSL(3, GaloisField p k))) ∨
    (∃ p k : ℕ, ∃ _hp : Fact p.Prime, 0 < k ∧ p ^ k % 4 = 1 ∧
        Nonempty (G ≃* PSU3 p k)) ∨
    Nonempty (G ≃* M11)

The files of 4 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.

Sources
LeanCFSG.Milestones.lr_semidihedral_simple_recognition_1 · CFSG.Milestones.lr_semidihedral_simple_recognition_2
Uses 4 · Used by 4
Statement usesFAM_classical_model_membership · LR_Glauberman_Z_star_central_Sylow_involution · LR_dihedral_simple_recognition · OO_odd_order_solvable
Used byCL_LIT_Aschbacher_component_type_theorem_5 · CL_LIT_Gorenstein_Walter_L_balance · CT_even_standard_residual_reduction · CT_rank_two_standard_recognition_frontier

TheoremLR_wreathed_simple_recognition#

The milestone module CFSG.Milestones.LR_wreathed_simple_recognition, one of those CFSG/Milestones.lean imports.

It declares 2 results, quoted from CFSG/Milestones/LR_wreathed_simple_recognition.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Milestones.lr_wreathed_simple_recognition_1 (theorem, line 61). Proved here.

theorem _root_.CFSG.Milestones.lr_wreathed_simple_recognition_1
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a)
    (hwr : ∃ (S : Sylow 2 G) (n : ℕ), 2 ≤ n ∧
      Nonempty ((S : Subgroup G) ≃* WreathedTwoGroup n)) :
    (∃ p f : ℕ, p.Prime ∧ p ≠ 2 ∧ 1 ≤ f ∧ p ^ f % 4 = 1 ∧
        StatedClassicalModel G .PSL 3 p f) ∨
    (∃ p f : ℕ, p.Prime ∧ p ≠ 2 ∧ 1 ≤ f ∧ p ^ f % 4 = 3 ∧
        StatedClassicalModel G .PSU 3 p f)

CFSG.Milestones.lr_wreathed_simple_recognition_2 (theorem, line 79). Proved here.

theorem _root_.CFSG.Milestones.lr_wreathed_simple_recognition_2
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a)
    (P : Sylow 2 G)
    (hwr : ∃ n : ℕ, 2 ≤ n ∧ Nonempty ((P : Subgroup G) ≃* WreathedTwoGroup n)) :
    (∃ p k : ℕ, ∃ _hp : Fact p.Prime, 0 < k ∧ p ^ k % 4 = 1 ∧
        Nonempty (G ≃* PSL(3, GaloisField p k))) ∨
    (∃ p k : ℕ, ∃ _hp : Fact p.Prime, 0 < k ∧ p ^ k % 4 = 3 ∧
        Nonempty (G ≃* PSU3 p k))

The files of 4 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.

Sources
LeanCFSG.Milestones.lr_wreathed_simple_recognition_1 · CFSG.Milestones.lr_wreathed_simple_recognition_2
Uses 4 · Used by 2
Statement usesFAM_classical_model_membership · LR_Glauberman_Z_star_central_Sylow_involution · LR_dihedral_simple_recognition · OO_odd_order_solvable
Used byQT_faithful_local_empty_classification · QTFE_unique_centralizer_six_model_recognition

TheoremOO_odd_order_solvable#

The milestone module CFSG.Milestones.OO_odd_order_solvable, one of those CFSG/Milestones.lean imports.

It declares 1 result, quoted from CFSG/Milestones/OO_odd_order_solvable.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Milestones.odd_order_solvable (theorem, line 11). Proved here.

theorem _root_.CFSG.Milestones.odd_order_solvable {G : Type*} [Group G] [Finite G]
    (_h : Odd (Nat.card G)) : Group.IsSolvable G

The files of 6 case theorems import it, directly or through other files: 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.

Sources
LeanCFSG.Milestones.odd_order_solvable
Uses 1 · Used by 6
Statement usesCFSG.FeitThompson.isSolvable_of_odd_natCard
Used byCLS_component_free_involution_odd_cores_trivial · CL_LIT_signalizer_functor_theorem · GW_original_post_proposition_sixteen_all_prime_stationarity_and_no_growth · LR_rank_two_isomorphism_types · LR_semidihedral_simple_recognition · LR_wreathed_simple_recognition

TheoremQTFE_unique_centralizer_six_model_recognition#

The milestone module CFSG.Milestones.QTFE_unique_centralizer_six_model_recognition, one of those CFSG/Milestones.lean imports.

It declares 1 result, quoted from CFSG/Milestones/QTFE_unique_centralizer_six_model_recognition.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Milestones.qtfe_unique_centralizer_six_model_recognition (theorem, line 637). Proved here.

theorem qtfe_unique_centralizer_six_model_recognition
    (G : Type) [Group G] [Finite G] (T Mc : Subgroup G)
    (hQTFE : CFSG.Quasithin.quasithinQTFE14Cat G T Mc) :
    Nonempty (G ≃* NativeSporadic.J2) ∨
    Nonempty (G ≃* NativeSporadic.J3) ∨
    LieModel G .trialityD4 0 2 1 ∨
    LieModel G .Tits 0 2 1 ∨
    (∃ (k : Type) (_ : Field k) (_ : Finite k), Nat.card k = 2 ∧
      Nonempty (G ≃* ↥⁅adjointGroup .G2 k, adjointGroup .G2 k⁆)) ∨
    Nonempty (G ≃* NativeSporadic.M12)

No case theorem's file imports it, directly or through other files.

Sources
LeanCFSG.Milestones.qtfe_unique_centralizer_six_model_recognition
Uses 11
Statement usesCFSG.Assembly.disconnected_involution_graph · AT_alternating_automorphism_permutation · CLS_component_dichotomy · CL_LIT_Fischer_3T_existence_uniqueness · CL_LIT_Goldschmidt_strongly_closed_abelian_models · CL_LIT_Griess_Schur_multipliers_Lie_type · CL_LIT_SQTK_simple_list · CT_catalog_nonabelian_type_partition · LR_Brauer_Suzuki_central_involution · LR_nonabelian_simple_two_rank_lower_bound · LR_wreathed_simple_recognition

TheoremQT_H13_maximal_local_catalog_assembly#

The milestone module CFSG.Milestones.QT_H13_maximal_local_catalog_assembly, one of those CFSG/Milestones.lean imports.

It declares 1 result, quoted from CFSG/Milestones/QT_H13_maximal_local_catalog_assembly.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Milestones.qt_h13_maximal_local_catalog_assembly (theorem, line 1778). Proved here.

theorem qt_h13_maximal_local_catalog_assembly
    (G : Type) [Group G] [Finite G] (T L : Subgroup G)
    (hH13 : CFSG.Quasithin.H13.QTH13 G T L)
    (hmax : CFSG.Open.quasithinIsMaximalLocal T L) : CFSG.Blueprint.Catalog G

The files of 1 case theorem import it, directly or through other files: CFSG.Assembly.quasithin.

Sources
LeanCFSG.Milestones.qt_h13_maximal_local_catalog_assembly
Uses 3 · Used by 1
Statement usesCL_LIT_Borel_Tits_local_parabolic · CL_LIT_Gorenstein_Walter_L_balance · QT_faithful_local_empty_classification
Used byQT_faithful_local_nonempty_classification

TheoremQT_faithful_local_empty_classification#

The milestone module CFSG.Milestones.QT_faithful_local_empty_classification, one of those CFSG/Milestones.lean imports.

It declares 1 result, quoted from CFSG/Milestones/QT_faithful_local_empty_classification.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Milestones.qt_faithful_local_empty_classification (theorem, line 638). Proved here.

theorem qt_faithful_local_empty_classification
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a) (hqtke : QuasithinUnique.quasithinIsQTKECat G)
    (T : Sylow 2 G)
    (hMT : ∃ M₁ M₂ : Subgroup G, M₁ ≠ M₂ ∧
      quasithinIsMaxTwoLocal M₁ ∧ quasithinIsMaxTwoLocal M₂ ∧
      (T : Subgroup G) ≤ M₁ ∧ (T : Subgroup G) ≤ M₂)
    (hLf : ∀ L : Subgroup G, ¬ quasithinIsFaithfulLocal (T : Subgroup G) L) :
    Blueprint.Catalog G

The files of 4 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.quasithin, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.

Sources
LeanCFSG.Milestones.qt_faithful_local_empty_classification
Uses 11 · Used by 2
Statement usesCFSG.Assembly.disconnected_involution_graph · AT_alternating_automorphism_permutation · CLS_component_dichotomy · CL_LIT_Fischer_3T_existence_uniqueness · CL_LIT_Goldschmidt_strongly_closed_abelian_models · CL_LIT_Griess_Schur_multipliers_Lie_type · CL_LIT_SQTK_simple_list · CT_catalog_nonabelian_type_partition · LR_Brauer_Suzuki_central_involution · LR_nonabelian_simple_two_rank_lower_bound · LR_wreathed_simple_recognition
Used byCL_LIT_GH74_sectional_two_rank_four · QT_H13_maximal_local_catalog_assembly

TheoremQT_faithful_local_nonempty_classification#

The milestone module CFSG.Milestones.QT_faithful_local_nonempty_classification, one of those CFSG/Milestones.lean imports.

It declares 1 result, quoted from CFSG/Milestones/QT_faithful_local_nonempty_classification.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Milestones.qt_faithful_local_nonempty_classification (theorem, line 1833). Proved here.

theorem _root_.CFSG.Milestones.qt_faithful_local_nonempty_classification
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a) (hqtke : quasithinIsQTKE G) (T : Sylow 2 G)
    (hLf : ∃ L : Subgroup G, quasithinIsFaithfulLocal (T : Subgroup G) L) :
    InCatalog G

The files of 1 case theorem import it, directly or through other files: CFSG.Assembly.quasithin.

Sources
LeanCFSG.Milestones.qt_faithful_local_nonempty_classification
Uses 1 · Used by 2
Statement usesQT_H13_maximal_local_catalog_assembly
Used byCFSG.Assembly.quasithin · CLS_QTKE_classification

TheoremQT_primitive_regular_cyclic_Burnside_Schur#

The milestone module CFSG.Milestones.QT_primitive_regular_cyclic_Burnside_Schur, one of those CFSG/Milestones.lean imports.

It declares 1 result, quoted from CFSG/Milestones/QT_primitive_regular_cyclic_Burnside_Schur.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:

CFSG.Milestones.burnside_schur (theorem, line 12). Proved here.

theorem _root_.CFSG.Milestones.burnside_schur {Ω : Type*} [Finite Ω] (G K : Subgroup (Equiv.Perm Ω))
    (hΩ : 2 ≤ Nat.card Ω) (hKG : K ≤ G) [IsPreprimitive G Ω] [IsCyclic K]
    [IsPretransitive K Ω] (hK : ∀ x : Ω, stabilizer K x = ⊥) :
    IsMultiplyPretransitive G Ω 2 ∨
      ∃ p : ℕ, p.Prime ∧ Nat.card Ω = p ∧ ∃ e : Ω ≃ ZMod p,
        e.permCongr '' (K : Set (Equiv.Perm Ω)) = {t | ∃ b, ∀ x, t x = x + b} ∧
        (∀ g ∈ G, ∃ a ≠ 0, ∃ b, ∀ x, e (g x) = a * e x + b) ∧
        (K.subgroupOf G).Normal

No case theorem's file imports it, directly or through other files.

Sources
LeanCFSG.Milestones.burnside_schur

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.