QT_unique_Shult_simple_strongly_… to ZJ_glauberman_replacement
TheoremQT_unique_Shult_simple_strongly_closed_TI_models#
The milestone module CFSG.Milestones.QT_unique_Shult_simple_strongly_closed_TI_models, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/QT_unique_Shult_simple_strongly_closed_TI_models.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.qt_unique_shult_simple_strongly_closed_ti_models (theorem, line 13). Proved here.
theorem _root_.CFSG.Milestones.qt_unique_shult_simple_strongly_closed_ti_models
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(T : Sylow 2 G) (U : Subgroup G) (hUT : U ≤ (T : Subgroup G)) (hU : U ≠ ⊥)
(hUel : IsElemAbelian 2 U)
(hclosed : fusionStronglyClosed (U : Set G) (T : Subgroup G))
(hTI : fusionIsTI U) :
fusionIsBenderGroup 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.
Uses 4 · Used by 4
TheoremQT_unique_maximal_local_classification#
The milestone module CFSG.Milestones.QT_unique_maximal_local_classification, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/QT_unique_maximal_local_classification.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.qt_unique_maximal_local_classification (theorem, line 415). Proved here.
theorem qt_unique_maximal_local_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)
(hT : ∃! M : Subgroup G, quasithinIsMaxTwoLocal M ∧ (T : Subgroup G) ≤ M) :
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.
Uses 7 · Used by 3
TheoremR3E_model_outcomes_catalog#
The milestone module CFSG.Milestones.R3E_model_outcomes_catalog, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/R3E_model_outcomes_catalog.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.r3e_model_outcomes_catalog (theorem, line 11). Proved here.
theorem r3e_model_outcomes_catalog (G : Type) [Group G]
(h : RankThreeIModel G ∨ RankThreeIIModel G) : Catalog G
No case theorem's file imports it, directly or through other files.
Uses 1
TheoremR3E_part_one_outcome_assembly#
The milestone module CFSG.Milestones.R3E_part_one_outcome_assembly, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/R3E_part_one_outcome_assembly.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.r3e_part_one_outcome_assembly (theorem, line 1901). Proved here.
theorem _root_.CFSG.Milestones.r3e_part_one_outcome_assembly
(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) (hq : ∃ q : ℕ, q.Prime ∧ 3 < q ∧ localRank q G = 3) :
IModel G ∨ AschCoreLocal G 2
The files of 1 case theorem import it, directly or through other files: CFSG.Assembly.rank_three_even.
Uses 1 · Used by 1
TheoremR3E_part_two_prime_three_outcome#
The milestone module CFSG.Milestones.R3E_part_two_prime_three_outcome, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/R3E_part_two_prime_three_outcome.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.r3e_part_two_prime_three_outcome (theorem, line 3141). Proved here.
theorem _root_.CFSG.Milestones.r3e_part_two_prime_three_outcome
(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) (hq : ∀ q : ℕ, q.Prime → 3 < q → localRank q G < 3) :
IIModel G ∨ AschCoreLocal G 2
The files of 1 case theorem import it, directly or through other files: CFSG.Assembly.rank_three_even.
Uses 4 · Used by 1
TheoremR3E_rank_three_core_uniqueness_exclusion#
The milestone module CFSG.Milestones.R3E_rank_three_core_uniqueness_exclusion, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/R3E_rank_three_core_uniqueness_exclusion.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.r3e_rank_three_core_uniqueness_exclusion (theorem, line 3615). Proved here.
theorem _root_.CFSG.Milestones.r3e_rank_three_core_uniqueness_exclusion
(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) : ¬ AschCoreLocal G 2
The files of 1 case theorem import it, directly or through other files: CFSG.Assembly.rank_three_even.
Uses 2 · Used by 1
TheoremSE_simple_strong_embedding_models#
The milestone module CFSG.Milestones.SE_simple_strong_embedding_models, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/SE_simple_strong_embedding_models.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.bender_suzuki (theorem, line 12). Proved here.
theorem _root_.CFSG.Milestones.bender_suzuki {X : Type*} [Group X] [Finite X] [IsSimpleGroup X]
(M : Subgroup X) (h : CFSG.BenderSuzuki.IsStronglyEmbeddedOrder M) :
CFSG.BenderSuzuki.IsBenderGroup 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.
Used by 1
TheoremSG_two_signalizer_completeness#
The milestone module CFSG.Milestones.SG_two_signalizer_completeness, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/SG_two_signalizer_completeness.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.sg_two_signalizer_completeness (theorem, line 46). Proved here.
theorem _root_.CFSG.Milestones.sg_two_signalizer_completeness
(G : Type) [Group G] [Finite G]
(A : Type) [CommGroup A] [Finite A] (hexp : ∀ a : A, a ^ 2 = 1) (hcard : 8 ≤ Nat.card A)
(α : A →* MulAut G) (θ : A → Subgroup G)
(hinv : ∀ a : A, a ≠ 1 → ∀ b : A, (θ a).map (α b).toMonoidHom = θ a)
(hsolv : ∀ a : A, a ≠ 1 → Group.IsSolvable (θ a))
(hodd : ∀ a : A, a ≠ 1 → Odd (Nat.card (θ a)))
(hcent : ∀ a : A, a ≠ 1 → ∀ g ∈ θ a, α a g = g)
(hbal : ∀ a b : A, a ≠ 1 → b ≠ 1 → ∀ g ∈ θ a, α b g = g → g ∈ θ b) :
let Θ : Subgroup G := ⨆ (a : A) (_ : a ≠ 1), θ a
(∀ b : A, Θ.map (α b).toMonoidHom = Θ) ∧ Group.IsSolvable Θ ∧ Odd (Nat.card Θ) ∧
∀ a : A, a ≠ 1 → ∀ g : G, (g ∈ Θ ∧ α a g = g ↔ g ∈ θ a)
The files of 3 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.
Used by 1
TheoremZJ_glauberman_characteristic#
The milestone module CFSG.Milestones.ZJ_glauberman_characteristic, one of those CFSG/Milestones.lean imports.
It declares 2 results, quoted from CFSG/Milestones/ZJ_glauberman_characteristic.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.zj_glauberman_characteristic_1 (theorem, line 12). Proved here.
theorem _root_.CFSG.Milestones.zj_glauberman_characteristic_1
(G : Type) [Group G] [Finite G]
(p : ℕ) (hp : p.Prime) (hodd : Odd p)
(hcharp : Subgroup.centralizer (pCore p G : Set G) ≤ pCore p G)
(S : Sylow p G)
(hstable : ∀ (P : Subgroup G) [P.Normal], IsPGroup p P → StatedConjPStable p P) :
((Subgroup.center (thompsonSubgroup (S : Subgroup G))).map
(thompsonSubgroup (S : Subgroup G)).subtype).Characteristic
CFSG.Milestones.zj_glauberman_characteristic_2 (theorem, line 28). Proved here.
theorem _root_.CFSG.Milestones.zj_glauberman_characteristic_2
(G : Type) [Group G] [Finite G]
(p : ℕ) (hp : p.Prime) (hodd : Odd p)
(hstable : CFSG.Open.IsPStable p G)
(hconstrained : Subgroup.centralizer (CFSG.Open.pCore p G : Set G) ≤ CFSG.Open.pCore p G)
(S : Sylow p G) :
((Subgroup.center (CFSG.Open.thompsonSubgroup (S : Subgroup G))).map
(CFSG.Open.thompsonSubgroup (S : Subgroup G)).subtype).Normal
The files of 3 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.
Used by 1
TheoremZJ_glauberman_replacement#
The milestone module CFSG.Milestones.ZJ_glauberman_replacement, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/ZJ_glauberman_replacement.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.glauberman_replacement (theorem, line 12). Proved here.
theorem _root_.CFSG.Milestones.glauberman_replacement {p : ℕ} (hp : Nat.Prime p) (hodd : Odd p)
{S : Type*} [Group S] [Finite S] (hS : IsPGroup p S) (B : Subgroup S) (hB : B.Normal)
(hclass : ⁅B, B⁆ ≤ (center B).map B.subtype) (hBZ : ⁅B, B⁆ ≤ thompsonCenter S) :
(∀ A ∈ maxOrderAbelianSubgroups S, B ≤ A) ∨
∃ A ∈ maxOrderAbelianSubgroups S, ¬ B ≤ A ∧ B ≤ normalizer (A : Set S)
No case theorem's file imports it, directly or through other files.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.