AT_alternating_automorphism_perm… to CLS_large_even_classification

TheoremAT_alternating_automorphism_permutation#

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

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

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

theorem _root_.CFSG.Milestones.alternating_automorphism_permutation {n : ℕ} (hn : n = 5 ∨ 7 ≤ n)
    (f : MulAut (alternatingGroup (Fin n))) :
    ∃ σ : Perm (Fin n), ∀ g : alternatingGroup (Fin n),
      (f g : Perm (Fin n)) = σ * (g : Perm (Fin n)) * σ⁻¹

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

• CFSG/Milestones/AT_alternating_automorphism_permutation.lean at 69cb972f

LeanCFSG.Milestones.alternating_automorphism_permutation

Used by 11

Used byCL_LIT_GMS_Monster_uniqueness · CL_LIT_Monster_existence_Griess_Conway · CL_LIT_signalizer_functor_theorem · CT_even_small_Lie_standard_frontier · CT_initial_standard_component_frontier · CT_rank_two_standard_recognition_frontier · FAM_M_finiteness · FAM_M_simplicity · QT_faithful_local_empty_classification · QTFE_unique_centralizer_six_model_recognition · QT_unique_maximal_local_classification

TheoremBI_Brauer_characterization#

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

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

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

theorem _root_.CFSG.Milestones.bi_brauer_characterization
    (G : Type) [Group G] [Finite G] (f : G → ℂ) (hf : BlocksIsClassFunction f) :
    f ∈ BlocksVChar G ↔
      ∀ E : Subgroup G, BlocksBrauerElementary E → (fun e : E => f e) ∈ BlocksVChar E

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

Sources

• CFSG/Milestones/BI_Brauer_characterization.lean at 69cb972f

LeanCFSG.Milestones.bi_brauer_characterization

TheoremBL_block_section_column_orthogonality#

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

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

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

theorem _root_.CFSG.Milestones.block_section_orthogonality (p : ℕ) (hp : p.Prime) (m : Ideal BlocksAlgInt) (hm : m.IsMaximal)
    (hpm : (p : BlocksAlgInt) ∈ m)
    (G : Type) [Group G] [Finite G] (B : Set (G → ℂ)) (hB : BlocksIsBlock m G B)
    (x y xp yp : G) (hx : BlocksIsPPart p x xp) (hy : BlocksIsPPart p y yp)
    (hxy : ¬ IsConj xp yp) :
    ∑ᶠ χ ∈ B, χ x * starRingEnd ℂ (χ y) = 0

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

Sources

• CFSG/Milestones/BL_block_section_column_orthogonality.lean at 69cb972f

LeanCFSG.Milestones.block_section_orthogonality

TheoremBT_principal_block_Brauer_correspondence#

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

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

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

theorem _root_.CFSG.Milestones.brauer_third_main_theorem (p : ℕ) (hp : p.Prime) (m : Ideal BlocksAlgInt) (hm : m.IsMaximal)
    (hpm : (p : BlocksAlgInt) ∈ m)
    (G : Type) [Group G] [Finite G] (P H : Subgroup G) (hP : IsPGroup p P)
    (hPH : P ≤ H) (hCH : Subgroup.centralizer (P : Set G) ≤ H)
    (hHN : H ≤ Subgroup.normalizer (P : Set G))
    (β : Set (H → ℂ)) (hβ : BlocksIsBlock m H β) :
    BlocksBrauerCorr m P H β (BlocksPrincipalBlock m G) ↔ β = BlocksPrincipalBlock m H

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

Sources

• CFSG/Milestones/BT_principal_block_Brauer_correspondence.lean at 69cb972f

LeanCFSG.Milestones.brauer_third_main_theorem

TheoremCAT_converse#

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

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

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

theorem cat_converse
    (G : Type) [Group G] (h : Blueprint.Catalog G) :
    Finite G ∧ IsSimpleGroup G

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

Sources

• CFSG/Milestones/CAT_converse.lean at 69cb972f

LeanCFSG.Milestones.cat_converse

Uses 1 · Used by 1

Statement usesFAM_sporadic_converse

Used byCFSG_classification

TheoremCAT_native_realization#

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

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

CFSG.Milestones.cat_native_realization_cyclic (theorem, line 34). Proved here.

theorem cat_native_realization_cyclic (p : ℕ) [Fact p.Prime] :
    Finite (Multiplicative (ZMod p)) ∧ IsSimpleGroup (Multiplicative (ZMod p))

CFSG.Milestones.cat_native_realization_alternating (theorem, line 39). Proved here.

theorem cat_native_realization_alternating (n : ℕ) (hn : 5 ≤ n) :
    Finite (alternatingGroup (Fin n)) ∧ IsSimpleGroup (alternatingGroup (Fin n))

CFSG.Milestones.cat_native_realization_lie (theorem, line 43). Proved here.

theorem cat_native_realization_lie
    (t : CFSG.Assembly.LowTwoRank.StatedLieTag) (n p f : ℕ)
    (h : CFSG.Assembly.LowTwoRank.StatedLieAdmissible t n p f) :
    ∃ (G : Type) (_ : Group G), Finite G ∧ Nontrivial G ∧ IsSimpleGroup G ∧
      CFSG.Blueprint.LieModel G t n p f

CFSG.Milestones.native_carrier_finite_simple_of_ne_B (theorem, line 51). Proved here.

theorem native_carrier_finite_simple_of_ne_B
    (s : TauCeti.SporadicName) (hs : s ≠ .B) :
    Finite (nativeCarrier s) ∧ Nontrivial (nativeCarrier s) ∧ IsSimpleGroup (nativeCarrier s)

CFSG.Milestones.cat_native_realization_cyclic' (theorem, line 89). Proved here.

theorem cat_native_realization_cyclic' (p : ℕ) (hp : p.Prime) :
    Finite (Multiplicative (ZMod p)) ∧ Nontrivial (Multiplicative (ZMod p)) ∧
      IsSimpleGroup (Multiplicative (ZMod p))

CFSG.Milestones.cat_native_realization_alternating' (theorem, line 96). Proved here.

theorem cat_native_realization_alternating' (n : ℕ) (hn : 5 ≤ n) :
    Finite (alternatingGroup (Fin n)) ∧ Nontrivial (alternatingGroup (Fin n)) ∧
      IsSimpleGroup (alternatingGroup (Fin n))

CFSG.Milestones.cat_native_realization_sporadic (theorem, line 103). Proved here.

theorem cat_native_realization_sporadic
    (s : TauCeti.SporadicName) :
    Finite (nativeCarrier s) ∧ Nontrivial (nativeCarrier s) ∧ IsSimpleGroup (nativeCarrier s)

CFSG.Milestones.cat_native_realization (theorem, line 113). Proved here.

theorem cat_native_realization :
    (∀ p : ℕ, p.Prime → Finite (Multiplicative (ZMod p)) ∧ Nontrivial (Multiplicative (ZMod p)) ∧
      IsSimpleGroup (Multiplicative (ZMod p))) ∧
    (∀ n : ℕ, 5 ≤ n → Finite (alternatingGroup (Fin n)) ∧ Nontrivial (alternatingGroup (Fin n)) ∧
      IsSimpleGroup (alternatingGroup (Fin n))) ∧
    (∀ (t : CFSG.Assembly.LowTwoRank.StatedLieTag) (n p f : ℕ),
      CFSG.Assembly.LowTwoRank.StatedLieAdmissible t n p f →
      ∃ (G : Type) (_ : Group G), Finite G ∧ Nontrivial G ∧ IsSimpleGroup G ∧
        CFSG.Blueprint.LieModel G t n p f) ∧
    (∀ s : TauCeti.SporadicName, Finite (nativeCarrier s) ∧ Nontrivial (nativeCarrier s) ∧
      IsSimpleGroup (nativeCarrier s))

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

Sources

• CFSG/Milestones/CAT_native_realization.lean at 69cb972f

LeanCFSG.Milestones.cat_native_realization_cyclic · CFSG.Milestones.cat_native_realization_alternating · CFSG.Milestones.cat_native_realization_lie · CFSG.Milestones.native_carrier_finite_simple_of_ne_B · CFSG.Milestones.cat_native_realization_cyclic' · CFSG.Milestones.cat_native_realization_alternating' · CFSG.Milestones.cat_native_realization_sporadic · CFSG.Milestones.cat_native_realization

Uses 2 · Used by 8

Statement usesFAM_Th_simplicity · FAM_classical_model_membership

Used byCL_LIT_Aschbacher_1983_uniqueness_case_rank_three · CL_LIT_GL83_Theorem_C_preuniqueness_rank_three · FAM_sporadic_native_converse · LC_GL_standard_type_recognition_rank_four · LC_GL_theorem_A · LC_GL_theorem_C_rank_four · LC_GL_uniqueness_exclusion_rank_four · R3E_part_two_prime_three_outcome

TheoremCFSG_classification#

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

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

CFSG.Milestones.cfsg_classification (theorem, line 4575). Proved here.

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

CFSG.Milestones.cfsg_classification_and_realization (theorem, line 4585). Proved here.

theorem cfsg_classification_and_realization
    :
    (∀ (G : Type) [Group G], Assembly.InCatalog G ↔ Finite G ∧ IsSimpleGroup G) ∧
    (∀ (p : ℕ) [Fact p.Prime],
      Finite (Multiplicative (ZMod p)) ∧ IsSimpleGroup (Multiplicative (ZMod p))) ∧
    (∀ n : ℕ, 5 ≤ n →
      Finite (alternatingGroup (Fin n)) ∧ IsSimpleGroup (alternatingGroup (Fin n))) ∧
    (∀ (t : CFSG.Assembly.LowTwoRank.StatedLieTag) (n p f : ℕ),
      CFSG.Assembly.LowTwoRank.StatedLieAdmissible t n p f →
      ∃ (H : Type) (_ : Group H), Finite H ∧ Nontrivial H ∧ IsSimpleGroup H ∧
        CFSG.Blueprint.LieModel H t n p f) ∧
    (∀ s : TauCeti.SporadicName, Finite (nativeCarrier s) ∧ Nontrivial (nativeCarrier s) ∧
      IsSimpleGroup (nativeCarrier s))

CFSG.Milestones.cfsg_classification_native_and_realization_of_certificates (theorem, line 4609). Proved here.

theorem cfsg_classification_native_and_realization_of_certificates
    :
    (∀ (G : Type) [Group G],
      Blueprint.NativeCatalog G ↔ Finite G ∧ Nontrivial G ∧ IsSimpleGroup G) ∧
    (∀ p : ℕ, p.Prime →
      Finite (Multiplicative (ZMod p)) ∧ Nontrivial (Multiplicative (ZMod p)) ∧
        IsSimpleGroup (Multiplicative (ZMod p))) ∧
    (∀ n : ℕ, 5 ≤ n →
      Finite (alternatingGroup (Fin n)) ∧ Nontrivial (alternatingGroup (Fin n)) ∧
        IsSimpleGroup (alternatingGroup (Fin n))) ∧
    (∀ (t : Assembly.LowTwoRank.StatedLieTag) (n p f : ℕ),
      Assembly.LowTwoRank.StatedLieAdmissible t n p f →
      ∃ (H : Type) (_ : Group H), Finite H ∧ Nontrivial H ∧ IsSimpleGroup H ∧
        Blueprint.LieModel H t n p f) ∧
    (∀ s : TauCeti.SporadicName, Finite (nativeCarrier s) ∧ Nontrivial (nativeCarrier s) ∧
      IsSimpleGroup (nativeCarrier s))

CFSG.Milestones.cfsg_classification_native_and_realization (theorem, line 4633). Proved here.

theorem cfsg_classification_native_and_realization :
    (∀ (G : Type) [Group G],
      Blueprint.NativeCatalog G ↔ Finite G ∧ Nontrivial G ∧ IsSimpleGroup G) ∧
    (∀ p : ℕ, p.Prime →
      Finite (Multiplicative (ZMod p)) ∧ Nontrivial (Multiplicative (ZMod p)) ∧
        IsSimpleGroup (Multiplicative (ZMod p))) ∧
    (∀ n : ℕ, 5 ≤ n →
      Finite (alternatingGroup (Fin n)) ∧ Nontrivial (alternatingGroup (Fin n)) ∧
        IsSimpleGroup (alternatingGroup (Fin n))) ∧
    (∀ (t : Assembly.LowTwoRank.StatedLieTag) (n p f : ℕ),
      Assembly.LowTwoRank.StatedLieAdmissible t n p f →
      ∃ (H : Type) (_ : Group H), Finite H ∧ Nontrivial H ∧ IsSimpleGroup H ∧
        Blueprint.LieModel H t n p f) ∧
    (∀ s : TauCeti.SporadicName, Finite (nativeCarrier s) ∧ Nontrivial (nativeCarrier s) ∧
      IsSimpleGroup (nativeCarrier s))

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

Sources

• CFSG/Milestones/CFSG_classification.lean at 69cb972f

LeanCFSG.Milestones.cfsg_classification · CFSG.Milestones.cfsg_classification_and_realization · CFSG.Milestones.cfsg_classification_native_and_realization_of_certificates · CFSG.Milestones.cfsg_classification_native_and_realization

Uses 3

Statement usesCAT_converse · CFSG_exhaustiveness · FAM_sporadic_native_converse

TheoremCFSG_exhaustiveness#

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

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

CFSG.Milestones.cfsg_exhaustiveness (theorem, line 3927). Proved here.

theorem cfsg_exhaustiveness
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G] :
    Blueprint.Catalog G

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

Sources

• CFSG/Milestones/CFSG_exhaustiveness.lean at 69cb972f

LeanCFSG.Milestones.cfsg_exhaustiveness

Uses 1 · Used by 1

Statement usesCLS_K_proper_simple_classification

Used byCFSG_classification

TheoremCLS_K_proper_simple_classification#

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

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

CFSG.Milestones.cls_k_proper_simple_classification (theorem, line 3931). Proved here.

theorem _root_.CFSG.Milestones.cls_k_proper_simple_classification
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hK : KProper InCatalog G) : InCatalog G

CFSG.Milestones.cls_k_proper_simple_classification_catalog (theorem, line 3939). Proved here.

theorem _root_.CFSG.Milestones.cls_k_proper_simple_classification_catalog
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hK : KCore.KProperAllSimple Blueprint.Catalog G) : Blueprint.Catalog G

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

Sources

• CFSG/Milestones/CLS_K_proper_simple_classification.lean at 69cb972f

LeanCFSG.Milestones.cls_k_proper_simple_classification · CFSG.Milestones.cls_k_proper_simple_classification_catalog

Uses 3 · Used by 1

Statement usesCFSG.Assembly.large_even · CFSG.Assembly.quasithin · CFSG.Assembly.rank_three_even

Used byCFSG_exhaustiveness

TheoremCLS_QTKE_classification#

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

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

CFSG.Milestones.cls_qtke_classification_even_characteristic (theorem, line 1866). Proved here.

theorem cls_qtke_classification_even_characteristic
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a)
    (hqtke : QuasithinUnique.quasithinIsQTKECat G) : Blueprint.Catalog G

CFSG.Milestones.cls_qtke_classification (theorem, line 1874). Proved here.

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

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

Sources

• CFSG/Milestones/CLS_QTKE_classification.lean at 69cb972f

LeanCFSG.Milestones.cls_qtke_classification_even_characteristic · CFSG.Milestones.cls_qtke_classification

Uses 2

Statement usesQT_faithful_local_nonempty_classification · QT_unique_maximal_local_classification

TheoremCLS_abelian_simple_catalog#

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

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

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

theorem _root_.CFSG.Milestones.cls_abelian_simple_catalog (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hcomm : ∀ a b : G, a * b = b * a) : InCatalog G

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

Sources

• CFSG/Milestones/CLS_abelian_simple_catalog.lean at 69cb972f

LeanCFSG.Milestones.cls_abelian_simple_catalog

TheoremCLS_characteristic_two_classification#

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

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

CFSG.Milestones.cls_characteristic_two_classification (theorem, line 3078). Proved here.

theorem _root_.CFSG.Milestones.cls_characteristic_two_classification
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a) (hK : KProper InCatalog G)
    (hchar : IsCharTwoType G) : InCatalog G

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

Sources

• CFSG/Milestones/CLS_characteristic_two_classification.lean at 69cb972f

LeanCFSG.Milestones.cls_characteristic_two_classification

Uses 3

Statement usesCFSG.Assembly.large_even · CFSG.Assembly.quasithin · CFSG.Assembly.rank_three_even

TheoremCLS_component_classification#

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

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

CFSG.Milestones.cls_component_classification (theorem, line 3082). Proved here.

theorem _root_.CFSG.Milestones.cls_component_classification
    (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

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

Sources

• CFSG/Milestones/CLS_component_classification.lean at 69cb972f

LeanCFSG.Milestones.cls_component_classification

Uses 1

Statement usesCFSG.Assembly.component_type

TheoremCLS_component_dichotomy#

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

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

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

theorem _root_.CFSG.Milestones.cls_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

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

• CFSG/Milestones/CLS_component_dichotomy.lean at 69cb972f

LeanCFSG.Milestones.cls_component_dichotomy

Uses 1 · Used by 4

Statement usesCFSG.Assembly.component_dichotomy

Used byCL_LIT_Gorenstein_Walter_L_balance · CT_even_standard_residual_reduction · QT_faithful_local_empty_classification · QTFE_unique_centralizer_six_model_recognition

TheoremCLS_component_free_centralizer_quotient_characteristic_two#

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

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

CFSG.Milestones.cls_component_free_centralizer_quotient_characteristic_two (theorem, line 53). Proved here.

theorem _root_.CFSG.Milestones.cls_component_free_centralizer_quotient_characteristic_two (G : Type) [Group G] [Finite G]
    (hcomp : ¬ IsComponentType G) (t : G) (ht : orderOf t = 2) :
    dichotomyCharP 2 (Subgroup.centralizer ({t} : Set G) ⧸
        oddCore (Subgroup.centralizer ({t} : Set G))) ∧
      (oddCore (Subgroup.centralizer ({t} : Set G)) = ⊥ →
        dichotomyCharP 2 (Subgroup.centralizer ({t} : Set G)))

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

Sources

• CFSG/Milestones/CLS_component_free_centralizer_quotient_characteristic_two.lean at 69cb972f

LeanCFSG.Milestones.cls_component_free_centralizer_quotient_characteristic_two

Used by 7

Used byCLS_component_free_involution_odd_cores_trivial · CL_LIT_Aschbacher_proper_two_generated_core · CL_LIT_signalizer_functor_theorem · GW_original_normalizer_R_pure_projective_shared_fourgroup_and_index_divisor · GW_original_post_proposition_sixteen_all_prime_stationarity_and_no_growth · GW_original_post_proposition_sixteen_canonical_stationary_prime_normalizers · QT_unique_maximal_local_classification

TheoremCLS_component_free_involution_odd_cores_trivial#

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

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

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

theorem _root_.CFSG.Milestones.cls_component_free_involution_odd_cores_trivial (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a) (hrank : 3 ≤ twoRank G)
    (hcomp : ¬ IsComponentType G) (hse : ∀ M : Subgroup G, ¬ dichotomyStronglyEmbedded M)
    (t : G) (ht : orderOf t = 2) :
    oddCore (Subgroup.centralizer ({t} : Set G)) = ⊥

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

Sources

• CFSG/Milestones/CLS_component_free_involution_odd_cores_trivial.lean at 69cb972f

LeanCFSG.Milestones.cls_component_free_involution_odd_cores_trivial

Uses 2 · Used by 4

Statement usesCLS_component_free_centralizer_quotient_characteristic_two · OO_odd_order_solvable

Used byCFSG.Assembly.component_dichotomy · CL_LIT_Aschbacher_component_type_theorem_5 · CL_LIT_Goldschmidt_strongly_closed_abelian · CL_LIT_Goldschmidt_strongly_closed_abelian_models

TheoremCLS_connectivity_MacWilliams_four_generator#

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

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

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

theorem _root_.CFSG.Milestones.cls_connectivity_macwilliams_four_generator
    (S : Type) [Group S] [Finite S] (hS : IsPGroup 2 S)
    (hE : ∀ E : Subgroup S, E.Normal → IsElemAbelian 2 E → Nat.card E ≠ 8) :
    ∀ U : Subgroup S, ∃ X : Finset S, X.card ≤ 4 ∧ Subgroup.closure (X : Set S) = U

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

• CFSG/Milestones/CLS_connectivity_MacWilliams_four_generator.lean at 69cb972f

LeanCFSG.Milestones.cls_connectivity_macwilliams_four_generator

Used by 5

Used byCL_LIT_signalizer_functor_theorem · CL_LIT_Timmesfeld_root_involutions · CL_LIT_Walter_abelian_Sylow_two_simple · LR_rank_two_isomorphism_types · QT_unique_Shult_simple_strongly_closed_TI_models

TheoremCLS_disconnected_simple_involution_graph_classification#

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

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

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

theorem _root_.CFSG.Milestones.cls_disconnected_simple_involution_graph_classification (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

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

Sources

• CFSG/Milestones/CLS_disconnected_simple_involution_graph_classification.lean at 69cb972f

LeanCFSG.Milestones.cls_disconnected_simple_involution_graph_classification

Uses 1

Statement usesCFSG.Assembly.disconnected_involution_graph

TheoremCLS_involution_centralizers_characteristic_two_transfer#

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

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

CFSG.Milestones.cls_involution_centralizers_characteristic_two_transfer (theorem, line 15). Proved here.

theorem _root_.CFSG.Milestones.cls_involution_centralizers_characteristic_two_transfer (G : Type) [Group G] [Finite G]
    (hC : ∀ t : G, orderOf t = 2 → dichotomyCharP 2 (Subgroup.centralizer ({t} : Set G))) :
    IsCharTwoType G

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

Sources

• CFSG/Milestones/CLS_involution_centralizers_characteristic_two_transfer.lean at 69cb972f

LeanCFSG.Milestones.cls_involution_centralizers_characteristic_two_transfer

Used by 2

Used byCFSG.Assembly.component_dichotomy · CT_Seitz_centerless_reduction_frontier

TheoremCLS_large_even_classification#

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

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

CFSG.Milestones.cls_large_even_classification (theorem, line 3029). Proved here.

theorem _root_.CFSG.Milestones.cls_large_even_classification
    (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

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

Sources

• CFSG/Milestones/CLS_large_even_classification.lean at 69cb972f

LeanCFSG.Milestones.cls_large_even_classification

Uses 1

Statement usesCFSG.Assembly.large_even

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.