CL_LIT_SQTK_simple_listBase to CT_rank_two_standard_recognition…
TheoremCL_LIT_SQTK_simple_listBase#
The milestone module CFSG.Milestones.CL_LIT_SQTK_simple_listBase, which CFSG/Milestones.lean does not import.
It declares 3 results, quoted from CFSG/Milestones/CL_LIT_SQTK_simple_listBase.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.SQTKSimpleList (def, line 12). A definition.
def SQTKSimpleList (S : Type) [Group S] : Prop
CFSG.Milestones.cl_lit_sqtk_simple_list (theorem, line 33). Proved here.
theorem cl_lit_sqtk_simple_list
(S : Type) [Group S] [Finite S]
(hnonab : ∃ a b : S, a * b ≠ b * a) (hSQT : IsStronglyQuasithin S) (hcat : Catalog S) :
SQTKSimpleList S
CFSG.Milestones.cl_lit_sqtk_simple_list_simple (theorem, line 39). Proved here.
theorem cl_lit_sqtk_simple_list_simple
(S : Type) [Group S] [Finite S] [IsSimpleGroup S]
(hnonab : ∃ a b : S, a * b ≠ b * a) (hSQTK : IsSQTKCat S) : SQTKSimpleList S
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 1 · Used by 4
TheoremCL_LIT_Steinberg_presentation_theorem#
The milestone module CFSG.Milestones.CL_LIT_Steinberg_presentation_theorem, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/CL_LIT_Steinberg_presentation_theorem.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_steinberg_presentation_theorem (theorem, line 12). Proved here.
theorem cl_lit_steinberg_presentation_theorem (t : CFSG.Assembly.LowTwoRank.StatedLieTag)
(n p f : ℕ) [Fact p.Prime] (hadm : CFSG.Assembly.LowTwoRank.StatedLieAdmissible t n p f)
(hrank : 3 ≤ bnRank t n) :
PresentationA.{0, 0, w} (bnRootSystem (lieUniversal t n p f hadm.1))
(lieUniversal t n p f hadm.1).D.rootGroup ∧
(IsUntwistedTag t →
IsParametrization (Φ := bnRootSystem (lieUniversal t n p f hadm.1))
(lieUniversal t n p f hadm.1).D.rootGroup (untwistedParam t n p f hadm.1) ∧
Nonempty (CommOrder (bnRootSystem (lieUniversal t n p f hadm.1))) ∧
PresentationB (Φ := bnRootSystem (lieUniversal t n p f hadm.1))
(untwistedParam t n p f hadm.1) ∧
RedundantR2 (bnRootSystem (lieUniversal t n p f hadm.1))
(lieUniversal t n p f hadm.1).D.rootGroup)
No case theorem's file imports it, directly or through other files.
Uses 1
TheoremCL_LIT_Stroth_Leon_Sims_Baby_Monster_recognition#
The milestone module CFSG.Milestones.CL_LIT_Stroth_Leon_Sims_Baby_Monster_recognition, one of those CFSG/Milestones.lean imports.
It declares 2 results, quoted from CFSG/Milestones/CL_LIT_Stroth_Leon_Sims_Baby_Monster_recognition.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_stroth_leon_sims_baby_monster_recognition (theorem, line 17). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_stroth_leon_sims_baby_monster_recognition :
∃ (B : Type) (_ : Group B) (_ : Finite B), IsSimpleGroup B ∧
Nat.card B = sporadicOrderBabyMonster ∧
∃ d₀ : B, orderOf d₀ = 2 ∧
Nat.card (Subgroup.centralizer ({d₀} : Set B)) = 4 * sporadicOrderTwistedE6Two ∧
∀ (G : Type) [Group G] [Finite G], IsSimpleGroup G →
∀ d : G, orderOf d = 2 →
Nonempty (Subgroup.centralizer ({d} : Set G) ≃*
Subgroup.centralizer ({d₀} : Set B)) →
Nonempty (G ≃* B)
CFSG.Milestones.cl_lit_stroth_leon_sims_baby_monster_recognition_models (theorem, line 36). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_stroth_leon_sims_baby_monster_recognition_models
(d₀ : Blueprint.NativeSporadic.B) (hd₀ : orderOf d₀ = 2)
(hrank : Matrix.rank (d₀.val.val - 1) = 1860)
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(d : G) (hd : orderOf d = 2)
(hcentralizer : Nonempty (Subgroup.centralizer ({d} : Set G) ≃*
Subgroup.centralizer ({d₀} : Set Blueprint.NativeSporadic.B))) :
Nonempty (G ≃* Blueprint.NativeSporadic.B)
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 1 · Used by 6
TheoremCL_LIT_Timmesfeld_1978_large_extraspecial#
The milestone module CFSG.Milestones.CL_LIT_Timmesfeld_1978_large_extraspecial, one of those CFSG/Milestones.lean imports.
It declares 2 results, quoted from CFSG/Milestones/CL_LIT_Timmesfeld_1978_large_extraspecial.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_timmesfeld_1978_large_extraspecial (theorem, line 498). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_timmesfeld_1978_large_extraspecial
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(z : G) (hz : orderOf z = 2)
(hext : timmesfeldIsExtraspecial (timmesfeldFStar (Subgroup.centralizer ({z} : Set G))))
(w : ℕ)
(hw : Nat.card (timmesfeldFStar (Subgroup.centralizer ({z} : Set G))) = 2 ^ (1 + 2 * w))
(Mbar : Type) [Group Mbar]
(hMbar : timmesfeldQuotientIso (timmesfeldFStar (Subgroup.centralizer ({z} : Set G))) Mbar) :
w ≤ 4 ∨
(Nonempty (G ≃* PSL(w + 2, ZMod 2)) ∨ Nonempty (G ≃* timmesfeldPSU (w + 2))) ∨
(6 ≤ w ∧ Even w ∧
∃ q : QuadraticForm (ZMod 2) (Fin w → ZMod 2), timmesfeldNondegenerate q ∧
(Nonempty (Mbar ≃* Equiv.Perm (Fin 3) × timmesfeldOmega q) ∨
Nonempty (Mbar ≃* Equiv.Perm (Fin 3) × timmesfeldIsometries q))) ∨
(w = 6 ∧ IsQuasisimple (timmesfeldLayer Mbar) ∧ Nat.card (timmesfeldOddCore Mbar) ≤ 3 ∧
∃ t : Mbar, orderOf t = 2 ∧
∃ R : Subgroup Mbar, R ≤ Subgroup.centralizer ({t} : Set Mbar) ∧
(R.subgroupOf (Subgroup.centralizer ({t} : Set Mbar))).Normal ∧
(frattini (pCoreOf 2 R)).map (pCoreOf 2 R).subtype ≤ Subgroup.zpowers t ∧
(timmesfeldQuotientIso (pCore 2 R) PSL(3, ZMod 2) ∨
(∃ q : QuadraticForm (ZMod 2) (Fin 4 → ZMod 2), timmesfeldNondegenerate q ∧
timmesfeldPlusType q ∧ timmesfeldQuotientIso (pCore 2 R) (timmesfeldOmega q)) ∨
(pCoreOf 2 R = Subgroup.zpowers t ∧
∃ q : QuadraticForm (ZMod 2) (Fin 6 → ZMod 2), timmesfeldNondegenerate q ∧
timmesfeldQuotientIso (pCore 2 R) (timmesfeldOmega q)))) ∨
(w = 10 ∧ (timmesfeldFStar Mbar).index ≤ 2 ∧
(Nonempty (timmesfeldFStar Mbar ≃* PSL(6, ZMod 2)) ∨
Nonempty (timmesfeldFStar Mbar ≃* timmesfeldPSU 6))) ∨
(w = 11 ∧ IsSimpleGroup Mbar ∧ Nat.card Mbar = timmesfeldOrderCo2) ∨
(w = 12 ∧ IsSimpleGroup Mbar ∧ Nat.card Mbar = timmesfeldOrderCo1) ∨
(IsSimpleGroup Mbar ∧ ∃ t : Mbar, orderOf t = 2 ∧
timmesfeldIsExtraspecial (timmesfeldFStar (Subgroup.centralizer ({t} : Set Mbar))) ∧
((w = 16 ∧ Nat.card (timmesfeldFStar (Subgroup.centralizer ({t} : Set Mbar))) = 2 ^ 17 ∧
timmesfeldQuotientIso (timmesfeldFStar (Subgroup.centralizer ({t} : Set Mbar)))
(Equiv.Perm (Fin 3) × timmesfeldOmegaPlus 4)) ∨
(w = 28 ∧ Nat.card (timmesfeldFStar (Subgroup.centralizer ({t} : Set Mbar))) = 2 ^ 33 ∧
timmesfeldQuotientIso (timmesfeldFStar (Subgroup.centralizer ({t} : Set Mbar)))
(timmesfeldOmegaPlus 6))))
CFSG.Milestones.cl_lit_timmesfeld_1978_large_extraspecial_models (theorem, line 548). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_timmesfeld_1978_large_extraspecial_models
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(z : G) (hz : orderOf z = 2)
(hext : timmesfeldIsExtraspecial (timmesfeldFStar (Subgroup.centralizer ({z} : Set G))))
(w : ℕ)
(hw : Nat.card (timmesfeldFStar (Subgroup.centralizer ({z} : Set G))) = 2 ^ (1 + 2 * w))
(Mbar : Type) [Group Mbar]
(hMbar : timmesfeldQuotientIso (timmesfeldFStar (Subgroup.centralizer ({z} : Set G))) Mbar) :
w ≤ 4 ∨
(Nonempty (G ≃* PSL(w + 2, ZMod 2)) ∨ Nonempty (G ≃* timmesfeldPSU (w + 2))) ∨
(6 ≤ w ∧ Even w ∧
∃ q : QuadraticForm (ZMod 2) (Fin w → ZMod 2), timmesfeldNondegenerate q ∧
(Nonempty (Mbar ≃* Equiv.Perm (Fin 3) × timmesfeldOmega q) ∨
Nonempty (Mbar ≃* Equiv.Perm (Fin 3) × timmesfeldIsometries q))) ∨
(w = 6 ∧ IsQuasisimple (timmesfeldLayer Mbar) ∧ Nat.card (timmesfeldOddCore Mbar) ≤ 3 ∧
∃ t : Mbar, orderOf t = 2 ∧
∃ R : Subgroup Mbar, R ≤ Subgroup.centralizer ({t} : Set Mbar) ∧
(R.subgroupOf (Subgroup.centralizer ({t} : Set Mbar))).Normal ∧
(frattini (pCoreOf 2 R)).map (pCoreOf 2 R).subtype ≤ Subgroup.zpowers t ∧
(timmesfeldQuotientIso (pCore 2 R) PSL(3, ZMod 2) ∨
(∃ q : QuadraticForm (ZMod 2) (Fin 4 → ZMod 2), timmesfeldNondegenerate q ∧
timmesfeldPlusType q ∧ timmesfeldQuotientIso (pCore 2 R) (timmesfeldOmega q)) ∨
(pCoreOf 2 R = Subgroup.zpowers t ∧
∃ q : QuadraticForm (ZMod 2) (Fin 6 → ZMod 2), timmesfeldNondegenerate q ∧
timmesfeldQuotientIso (pCore 2 R) (timmesfeldOmega q)))) ∨
(w = 10 ∧ (timmesfeldFStar Mbar).index ≤ 2 ∧
(Nonempty (timmesfeldFStar Mbar ≃* PSL(6, ZMod 2)) ∨
Nonempty (timmesfeldFStar Mbar ≃* timmesfeldPSU 6)) ∧
∃ σ : Mbar, σ * σ = 1 ∧
timmesfeldFStar Mbar ⊔ Subgroup.zpowers σ = ⊤) ∨
(w = 11 ∧ Nonempty (Mbar ≃* Blueprint.NativeSporadic.Co2)) ∨
(w = 12 ∧ Nonempty (Mbar ≃* Blueprint.NativeSporadic.Co1)) ∨
(IsSimpleGroup Mbar ∧ ∃ t : Mbar, orderOf t = 2 ∧
timmesfeldIsExtraspecial (timmesfeldFStar (Subgroup.centralizer ({t} : Set Mbar))) ∧
((w = 16 ∧ Nat.card (timmesfeldFStar (Subgroup.centralizer ({t} : Set Mbar))) = 2 ^ 17 ∧
timmesfeldQuotientIso (timmesfeldFStar (Subgroup.centralizer ({t} : Set Mbar)))
(Equiv.Perm (Fin 3) × timmesfeldOmegaPlus 4)) ∨
(w = 28 ∧ Nat.card (timmesfeldFStar (Subgroup.centralizer ({t} : Set Mbar))) = 2 ^ 33 ∧
timmesfeldQuotientIso (timmesfeldFStar (Subgroup.centralizer ({t} : Set Mbar)))
(timmesfeldOmegaPlus 6))))
The files of 2 case theorems import it, directly or through other files: CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.
Uses 2 · Used by 6
TheoremCL_LIT_Timmesfeld_root_involutions#
The milestone module CFSG.Milestones.CL_LIT_Timmesfeld_root_involutions, one of those CFSG/Milestones.lean imports.
It declares 2 results, quoted from CFSG/Milestones/CL_LIT_Timmesfeld_root_involutions.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_timmesfeld_root_involutions (theorem, line 12). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_timmesfeld_root_involutions
(G : Type) [Group G] [Finite G] (D : Set G)
(hclass : ∃ d₀ : G, D = {g | IsConj d₀ g})
(hinv : ∀ d ∈ D, orderOf d = 2)
(hgen : Subgroup.closure D = ⊤)
(hcenter : Subgroup.center G = ⊥)
(hodd : ∀ N : Subgroup G, N.Normal → Odd (Nat.card N) → N = ⊥)
(hO2 : ∀ N : Subgroup G, N.Normal → IsPGroup 2 N → N = ⊥)
(hprod : ∀ d ∈ D, ∀ e ∈ D,
orderOf (d * e) = 2 ∨ orderOf (d * e) = 4 ∨ Odd (orderOf (d * e)))
(hfour : ∀ d ∈ D, ∀ e ∈ D, orderOf (d * e) = 4 → (d * e) ^ 2 ∈ D)
(hnondeg : ∃ d ∈ D, ∃ e ∈ D, orderOf (d * e) = 4) :
IsSimpleGroup G ∧
((Nat.card G ∈ lieOrdersChar 2 ∧
(∀ n f : ℕ, 2 ≤ n → 1 ≤ f → Nat.card G ≠ ordTwistedA n (2 ^ f)) ∧
(∀ f : ℕ, 1 ≤ f → Nat.card G ≠ ordBC 2 (2 ^ f))) ∨
Nonempty (G ≃* PSU3 3 1) ∨
Nonempty (G ≃* alternatingGroup (Fin 6)) ∨
Nat.card G = 2 ^ 7 * 3 ^ 3 * 5 ^ 2 * 7)
CFSG.Milestones.cl_lit_timmesfeld_root_involutions_models (theorem, line 39). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_timmesfeld_root_involutions_models
(G : Type) [Group G] [Finite G] (D : Set G)
(hclass : ∃ d₀ : G, D = {g | IsConj d₀ g})
(hinv : ∀ d ∈ D, orderOf d = 2)
(hgen : Subgroup.closure D = ⊤)
(hcenter : Subgroup.center G = ⊥)
(hodd : ∀ N : Subgroup G, N.Normal → Odd (Nat.card N) → N = ⊥)
(hO2 : ∀ N : Subgroup G, N.Normal → IsPGroup 2 N → N = ⊥)
(hprod : ∀ d ∈ D, ∀ e ∈ D,
orderOf (d * e) = 2 ∨ orderOf (d * e) = 4 ∨ Odd (orderOf (d * e)))
(hfour : ∀ d ∈ D, ∀ e ∈ D, orderOf (d * e) = 4 → (d * e) ^ 2 ∈ D)
(hnondeg : ∃ d ∈ D, ∃ e ∈ D, orderOf (d * e) = 4) :
(Blueprint.EvenLieType G ∧
(∀ n f : ℕ, 3 ≤ n → 1 ≤ f → ¬ Blueprint.LieModel G .PSU n 2 f) ∧
(∀ f : ℕ, 1 ≤ f → ¬ Blueprint.LieModel G .PSp 2 2 f)) ∨
Blueprint.LieModel G .PSU 3 3 1 ∨ Nonempty (G ≃* alternatingGroup (Fin 6)) ∨
Blueprint.NativeSporadic.IsSporadic G .J2
No case theorem's file imports it, directly or through other files.
TheoremCL_LIT_Walter_abelian_Sylow_two_simple#
The milestone module CFSG.Milestones.CL_LIT_Walter_abelian_Sylow_two_simple, one of those CFSG/Milestones.lean imports.
It declares 2 results, quoted from CFSG/Milestones/CL_LIT_Walter_abelian_Sylow_two_simple.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_walter_abelian_sylow_two_simple (theorem, line 16). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_walter_abelian_sylow_two_simple
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(P : Sylow 2 G) (hP : IsMulCommutative (P : Subgroup G)) :
(∃ f : ℕ, 2 ≤ f ∧ Nonempty (G ≃* PSL(2, GaloisField 2 f))) ∨
(∃ p f : ℕ, ∃ _hp : Fact p.Prime, Odd p ∧ 0 < f ∧ 5 ≤ p ^ f ∧
(p ^ f % 8 = 3 ∨ p ^ f % 8 = 5) ∧ Nonempty (G ≃* PSL(2, GaloisField p f))) ∨
(∃ m : ℕ, 1 ≤ m ∧ Nat.card G = ordRee (3 ^ (2 * m + 1))) ∨
Nonempty (G ≃* walterJ1)
CFSG.Milestones.cl_lit_walter_abelian_sylow_two_simple_models (theorem, line 33). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_walter_abelian_sylow_two_simple_models
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(P : Sylow 2 G) (hP : IsMulCommutative (P : Subgroup G)) :
(∃ f : ℕ, 2 ≤ f ∧ Blueprint.LieModel G .PSL 2 2 f) ∨
(∃ p f : ℕ, p.Prime ∧ p ≠ 2 ∧ 1 ≤ f ∧ 5 ≤ p ^ f ∧
(p ^ f % 8 = 3 ∨ p ^ f % 8 = 5) ∧ Blueprint.LieModel G .PSL 2 p f) ∨
(∃ f : ℕ, Odd f ∧ 3 ≤ f ∧ Blueprint.LieModel G .twistedG2 0 3 f) ∨
Blueprint.NativeSporadic.IsSporadic G .J1
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 3
TheoremCL_LIT_classical_involution_theorem#
The milestone module CFSG.Milestones.CL_LIT_classical_involution_theorem, one of those CFSG/Milestones.lean imports.
It declares 2 results, quoted from CFSG/Milestones/CL_LIT_classical_involution_theorem.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_classical_involution_theorem_models (theorem, line 1806). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_classical_involution_theorem_models
(G : Type) [Group G] [Finite G]
[IsSimpleGroup (genFittingFStar G)]
(hFnonab : ∃ a b : genFittingFStar G, a * b ≠ b * a)
(z : G) (hz : orderOf z = 2)
(J : Subgroup G) (hzJ : z ∈ J) (hJ : IsSubnormal J (Subgroup.centralizer ({z} : Set G)))
(S : Sylow 2 J)
(hS : ∃ r : ℕ, 3 ≤ r ∧ Nonempty ((S : Subgroup J) ≃* QuaternionGroup (2 ^ (r - 2)))) :
(classicalInvolutionWitness J → Blueprint.OddLieType (genFittingFStar G) ∨
Blueprint.NativeSporadic.IsSporadic (genFittingFStar G) .M11) ∧
(classicalInvolutionTightlyEmbedded J → Blueprint.OddLieType (genFittingFStar G) ∨
Blueprint.NativeSporadic.IsSporadic (genFittingFStar G) .M11 ∨
Blueprint.NativeSporadic.IsSporadic (genFittingFStar G) .M12)
CFSG.Milestones.cl_lit_classical_involution_theorem (theorem, line 1828). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_classical_involution_theorem
(G : Type) [Group G] [Finite G]
(F : Subgroup G) [F.Normal] [IsSimpleGroup F]
(hFnonab : ∃ a b : F, a * b ≠ b * a)
(hFstar : Subgroup.centralizer (F : Set G) = ⊥)
(z : G) (hz : orderOf z = 2)
(J : Subgroup G) (hzJ : z ∈ J) (hJ : IsSubnormal J (Subgroup.centralizer ({z} : Set G)))
(S : Sylow 2 J)
(hS : ∃ r : ℕ, 3 ≤ r ∧ Nonempty ((S : Subgroup J) ≃* QuaternionGroup (2 ^ (r - 2)))) :
(classicalInvolutionWitness J →
(∃ p : ℕ, p.Prime ∧ p ≠ 2 ∧ Nat.card F ∈ lieOrdersChar p) ∨ Nonempty (F ≃* M11)) ∧
(classicalInvolutionTightlyEmbedded J →
(∃ p : ℕ, p.Prime ∧ p ≠ 2 ∧ Nat.card F ∈ lieOrdersChar p) ∨ Nonempty (F ≃* M11) ∨
Nonempty (F ≃* classicalInvolutionM12))
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.
Uses 1 · Used by 7
TheoremCL_LIT_signalizer_functor_theorem#
The milestone module CFSG.Milestones.CL_LIT_signalizer_functor_theorem, one of those CFSG/Milestones.lean imports.
It declares 2 results, quoted from CFSG/Milestones/CL_LIT_signalizer_functor_theorem.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.cl_lit_signalizer_functor_theorem_1 (theorem, line 18). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_signalizer_functor_theorem_1
(G : Type) [Group G] [Finite G]
(p : ℕ) (hp : p.Prime) (k : ℕ) (hk : 1 ≤ k)
(A : Subgroup G) (hA : IsElemAbelian p A) (hrank : p ^ (k + 2) ≤ Nat.card A)
(Θ : Subgroup G → Subgroup G)
(hcent : ∀ S ∈ signalizerFunctorEk p k A, Θ S ≤ Subgroup.centralizer (S : Set G))
(hcop : ∀ S ∈ signalizerFunctorEk p k A, Nat.Coprime p (Nat.card (Θ S)))
(hinv : ∀ S ∈ signalizerFunctorEk p k A, A ≤ Subgroup.normalizer (Θ S : Set G))
(hbal : ∀ S ∈ signalizerFunctorEk p k A, ∀ S' ∈ signalizerFunctorEk p k A,
Θ S ⊓ Subgroup.centralizer (S' : Set G) ≤ Θ S')
(hK : ∀ S ∈ signalizerFunctorEk p k A, CFSG.SectionRank.IsKGroupCat ↥(Θ S)) :
let W : Subgroup G := ⨆ (S : Subgroup G) (_ : S ∈ signalizerFunctorEk p k A), Θ S
(Nat.Coprime p (Nat.card W) ∧ A ≤ Subgroup.normalizer (W : Set G)) ∧
(∀ S ∈ signalizerFunctorEk p k A, W ⊓ Subgroup.centralizer (S : Set G) = Θ S) ∧
(∀ Y : Subgroup G, A ≤ Subgroup.normalizer (Y : Set G) →
(∀ S ∈ signalizerFunctorEk p k A, Y ⊓ Subgroup.centralizer (S : Set G) ≤ Θ S) →
Y ≤ W) ∧
((∀ S ∈ signalizerFunctorEk p k A, Group.IsSolvable (Θ S)) → Group.IsSolvable W)
CFSG.Milestones.cl_lit_signalizer_functor_theorem_2 (theorem, line 46). Proved here.
theorem _root_.CFSG.Milestones.cl_lit_signalizer_functor_theorem_2
(G : Type) [Group G] [Finite G]
(p : ℕ) (hp : p.Prime)
(A : Subgroup G) (hA : IsMulCommutative A) (hexp : ∀ a ∈ A, a ^ p = 1)
(hrank : p ^ 3 ∣ Nat.card A)
(θ : G → Subgroup G) (hθ : IsSolvableSignalizerFunctor p A θ) :
let W : Subgroup G := ⨆ (a : G) (_ : a ∈ A) (_ : a ≠ 1), θ a
Nat.Coprime p (Nat.card W) ∧ Group.IsSolvable W ∧
∀ a ∈ A, a ≠ 1 → θ a = W ⊓ Subgroup.centralizer {a}
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 8 · Used by 2
TheoremCTB_KProper_component_local_B#
The milestone module CFSG.Milestones.CTB_KProper_component_local_B, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/CTB_KProper_component_local_B.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.ctb_kproper_component_local_b (theorem, line 2431). Proved here.
theorem _root_.CFSG.Milestones.ctb_kproper_component_local_b
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a) (hK : KProper CFSG.Blueprint.Catalog G)
(hcomp : IsComponentType G) : oddCore G = ⊥ ∧ LocalBProperty G
The files of 2 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.rank_three_even.
TheoremCTGMS_Bender_1971_even_rank_one_model_and_strong_embedding_input#
The milestone module CFSG.Milestones.CTGMS_Bender_1971_even_rank_one_model_and_strong_embedding_input, one of those CFSG/Milestones.lean imports.
It declares 4 results, quoted from CFSG/Milestones/CTGMS_Bender_1971_even_rank_one_model_and_strong_embedding_input.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.ctgms_bender_1971_even_rank_one_model_and_strong_embedding_input_1 (theorem, line 16). Proved here.
theorem _root_.CFSG.Milestones.ctgms_bender_1971_even_rank_one_model_and_strong_embedding_input_1 (f : ℕ) (hf : 2 ≤ f) :
fusionBenderBorel PSL(2, GaloisField 2 f) (2 ^ f) 1
CFSG.Milestones.ctgms_bender_1971_even_rank_one_model_and_strong_embedding_input_2 (theorem, line 26). Proved here.
theorem _root_.CFSG.Milestones.ctgms_bender_1971_even_rank_one_model_and_strong_embedding_input_2 (f : ℕ) (hf : 2 ≤ f) :
fusionBenderBorel (PSU3 2 f) (2 ^ f) 3
CFSG.Milestones.ctgms_bender_1971_even_rank_one_model_and_strong_embedding_input_3 (theorem, line 36). Proved here.
theorem _root_.CFSG.Milestones.ctgms_bender_1971_even_rank_one_model_and_strong_embedding_input_3
(X : Type) [Group X] [Finite X] (H : Subgroup X) (hH : fusionStronglyEmbedded H) :
(∀ S : Sylow 2 X, IsCyclic (S : Subgroup X) ∨
∃ r : ℕ, 3 ≤ r ∧ Nonempty ((S : Subgroup X) ≃* QuaternionGroup (2 ^ (r - 2)))) ∨
∃ (M N : Subgroup X) (_ : M.Normal) (_ : N.Normal) (_ : (M.subgroupOf N).Normal),
M ≤ N ∧ Odd (Nat.card M) ∧ Odd N.index ∧ fusionIsBenderGroup (N ⧸ M.subgroupOf N)
CFSG.Milestones.ctgms_bender_1971_even_rank_one_model_and_strong_embedding_input_4 (theorem, line 50). Proved here.
theorem _root_.CFSG.Milestones.ctgms_bender_1971_even_rank_one_model_and_strong_embedding_input_4 (a : ℕ) (ha : 1 ≤ a) :
fusionBenderBorel (Sz a) (2 ^ (2 * a + 1)) 2
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
TheoremCTSS_sporadic_standard_centerless_M12_J2_and_other_quotients_frontier#
The milestone module CFSG.Milestones.CTSS_sporadic_standard_centerless_M12_J2_and_other_quotients_frontier, one of those CFSG/Milestones.lean imports.
It declares 2 results, quoted from CFSG/Milestones/CTSS_sporadic_standard_centerless_M12_J2_and_other_quotients_frontier.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.ctss_sporadic_standard_centerless_m12_j2_and_other_quotients_frontier (theorem, line 3286). Proved here.
theorem _root_.CFSG.Milestones.ctss_sporadic_standard_centerless_m12_j2_and_other_quotients_frontier
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(hK : CFSG.Assembly.KProper CFSG.Blueprint.Catalog G)
(L : Subgroup G) (hL : standardComponentIsStandard L)
(hcore : ∀ t : G, orderOf t = 2 →
standardComponentOddCore (Subgroup.centralizer ({t} : Set G)) = ⊥)
(S : Sylow 2 (Subgroup.centralizer (L : Set G)))
(hS : IsCyclic (S : Subgroup (Subgroup.centralizer (L : Set G))))
(htype : Blueprint.Recognition.Exact.EvenStandardType (L ⧸ Subgroup.center L))
(hexc : ¬ Blueprint.Recognition.Exact.EvenStandardException (L ⧸ Subgroup.center L))
(hres : Blueprint.Recognition.Exact.EvenStandardResidual L)
(hspor : Blueprint.NativeSporadic.SporadicRep (L ⧸ Subgroup.center L))
(hMJ : Blueprint.NativeSporadic.IsSporadic (L ⧸ Subgroup.center L) .M12 ∨
Blueprint.NativeSporadic.IsSporadic (L ⧸ Subgroup.center L) .J2 → Subgroup.center L = ⊥) :
Nat.card G ∈ standardComponentEvenSporadicOrders
CFSG.Milestones.ctss_sporadic_standard_centerless_m12_j2_and_other_quotients_frontier_models (theorem, line 3328). Proved here.
theorem _root_.CFSG.Milestones.ctss_sporadic_standard_centerless_m12_j2_and_other_quotients_frontier_models
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(hK : CFSG.Assembly.KProper CFSG.Blueprint.Catalog G)
(L : Subgroup G) (hL : standardComponentIsStandard L)
(hcore : ∀ t : G, orderOf t = 2 →
standardComponentOddCore (Subgroup.centralizer ({t} : Set G)) = ⊥)
(S : Sylow 2 (Subgroup.centralizer (L : Set G)))
(hS : IsCyclic (S : Subgroup (Subgroup.centralizer (L : Set G))))
(htype : Blueprint.Recognition.Exact.EvenStandardType (L ⧸ Subgroup.center L))
(hexc : ¬ Blueprint.Recognition.Exact.EvenStandardException (L ⧸ Subgroup.center L))
(hres : Blueprint.Recognition.Exact.EvenStandardResidual L)
(hspor : Blueprint.NativeSporadic.SporadicRep (L ⧸ Subgroup.center L))
(hMJ : Blueprint.NativeSporadic.IsSporadic (L ⧸ Subgroup.center L) .M12 ∨
Blueprint.NativeSporadic.IsSporadic (L ⧸ Subgroup.center L) .J2 → Subgroup.center L = ⊥) :
Blueprint.Recognition.EvenSporadicOutcome G
The files of 2 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.rank_three_even.
Sources
Uses 8 · Used by 1
TheoremCTU_KProper_simple_unbalanced_recognition#
The milestone module CFSG.Milestones.CTU_KProper_simple_unbalanced_recognition, one of those CFSG/Milestones.lean imports.
It declares 3 results, quoted from CFSG/Milestones/CTU_KProper_simple_unbalanced_recognition.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.ctu_relativeU_catalog (theorem, line 2436). Proved here.
theorem _root_.CFSG.Milestones.ctu_relativeU_catalog
:
CFSG.ComponentClassification.KProperRelativeB.RelativeU CFSG.Blueprint.Catalog
CFSG.Milestones.ctu_kproper_simple_unbalanced_recognition (theorem, line 2458). Proved here.
theorem _root_.CFSG.Milestones.ctu_kproper_simple_unbalanced_recognition
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(hK : CFSG.Assembly.KProper CFSG.Blueprint.Catalog G)
(z : G) (hz : orderOf z = 2)
(hunbal : CFSG.oddCore (Subgroup.centralizer ({z} : Set G)) ≠ ⊥) :
CFSG.Blueprint.OddLieType G ∨
∃ n : ℕ, 7 ≤ n ∧ n % 4 = 3 ∧ Nonempty (G ≃* alternatingGroup (Fin n))
CFSG.Milestones.ctu_kproper_simple_unbalanced_recognition_models (theorem, line 2469). Proved here.
theorem _root_.CFSG.Milestones.ctu_kproper_simple_unbalanced_recognition_models
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(hK : CFSG.Assembly.KProper CFSG.Blueprint.Catalog G)
(z : G) (hz : orderOf z = 2)
(hunbal : CFSG.oddCore (Subgroup.centralizer ({z} : Set G)) ≠ ⊥) :
(CFSG.Blueprint.OddLieType G ∨
∃ n : ℕ, 7 ≤ n ∧ n % 4 = 3 ∧ Nonempty (G ≃* alternatingGroup (Fin n))) ∧
CFSG.Blueprint.Catalog G
The files of 2 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.rank_three_even.
TheoremCT_Seitz_centerless_reduction_frontier#
The milestone module CFSG.Milestones.CT_Seitz_centerless_reduction_frontier, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/CT_Seitz_centerless_reduction_frontier.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.ct_seitz_centerless_reduction_frontier (theorem, line 15). Proved here.
theorem _root_.CFSG.Milestones.ct_seitz_centerless_reduction_frontier
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(hK : CFSG.Assembly.KProper CFSG.Blueprint.Catalog G)
(L : Subgroup G) (hL : standardComponentIsStandard L)
(hcore : ∀ t : G, orderOf t = 2 →
standardComponentOddCore (Subgroup.centralizer ({t} : Set G)) = ⊥)
(S : Sylow 2 (Subgroup.centralizer (L : Set G)))
(hS : IsCyclic (S : Subgroup (Subgroup.centralizer (L : Set G))))
(htype : Blueprint.Recognition.Exact.EvenStandardType (L ⧸ Subgroup.center L))
(hexc : ¬ Blueprint.Recognition.Exact.EvenStandardException (L ⧸ Subgroup.center L))
(hZ : Subgroup.center L = ⊥) :
Blueprint.NativeSporadic.SporadicRep L ∨ Blueprint.Recognition.Exact.EvenBNRankTwoType L ∨
(Blueprint.LieModel L .PSp 3 2 1 ∨ Blueprint.LieModel L .PSU 6 2 1 ∨
Blueprint.LieModel L .POmegaMinus 4 2 1 ∨ Blueprint.LieModel L .POmegaPlus 4 2 1)
The files of 2 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.rank_three_even.
Uses 8 · Used by 1
TheoremCT_catalog_nonabelian_type_partition#
The milestone module CFSG.Milestones.CT_catalog_nonabelian_type_partition, one of those CFSG/Milestones.lean imports.
It declares 4 results, quoted from CFSG/Milestones/CT_catalog_nonabelian_type_partition.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Blueprint.suzukiModel_admissible (theorem, line 11). Proved here.
theorem suzukiModel_admissible {G : Type} [Group G] {p f : ℕ} (h : SuzukiModel G p f) :
StatedLieAdmissible .twistedB2 0 p f
CFSG.Blueprint.oddLieType_or_evenLieType_of_lieModel (theorem, line 16). Proved here.
theorem oddLieType_or_evenLieType_of_lieModel {X : Type} [Group X] {t : StatedLieTag}
{n p f : ℕ} (hadm : StatedLieAdmissible t n p f) (h : LieModel X t n p f) :
OddLieType X ∨ EvenLieType X
CFSG.Milestones.ct_catalog_nonabelian_type_partition_converse (theorem, line 35). Proved here.
theorem ct_catalog_nonabelian_type_partition_converse (X : Type) [Group X]
(h : (∃ n : ℕ, 5 ≤ n ∧ Nonempty (X ≃* alternatingGroup (Fin n))) ∨
OddLieType X ∨ EvenLieType X ∨ NativeSporadic.SporadicRep X) : Catalog X
CFSG.Milestones.ct_catalog_nonabelian_type_partition (theorem, line 44). Proved here.
theorem ct_catalog_nonabelian_type_partition (X : Type) [Group X]
(hnonab : ∃ a b : X, a * b ≠ b * a) :
Catalog X ↔
(∃ n : ℕ, 5 ≤ n ∧ Nonempty (X ≃* alternatingGroup (Fin n))) ∨
OddLieType X ∨ EvenLieType X ∨ NativeSporadic.SporadicRep X
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 1 · Used by 8
TheoremCT_even_small_Lie_standard_frontier#
The milestone module CFSG.Milestones.CT_even_small_Lie_standard_frontier, one of those CFSG/Milestones.lean imports.
It declares 2 results, quoted from CFSG/Milestones/CT_even_small_Lie_standard_frontier.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.ct_even_small_lie_standard_frontier (theorem, line 761). Proved here.
theorem _root_.CFSG.Milestones.ct_even_small_lie_standard_frontier
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(hK : CFSG.Assembly.KProper CFSG.Blueprint.Catalog G)
(L : Subgroup G) (hL : standardComponentIsStandard L)
(hcore : ∀ t : G, orderOf t = 2 →
standardComponentOddCore (Subgroup.centralizer ({t} : Set G)) = ⊥)
(S : Sylow 2 (Subgroup.centralizer (L : Set G)))
(hS : IsCyclic (S : Subgroup (Subgroup.centralizer (L : Set G))))
(htype : Blueprint.Recognition.Exact.EvenStandardType (L ⧸ Subgroup.center L))
(hexc : ¬ Blueprint.Recognition.Exact.EvenStandardException (L ⧸ Subgroup.center L))
(hres : Blueprint.Recognition.Exact.EvenStandardResidual L)
(hbcd : Blueprint.Recognition.Exact.ResidualB L ∨ Blueprint.Recognition.Exact.ResidualC L ∨
Blueprint.Recognition.Exact.ResidualD L) :
Nat.card G ∈ standardComponentEvenSporadicOrders
CFSG.Milestones.ct_even_small_lie_standard_frontier_models (theorem, line 783). Proved here.
theorem _root_.CFSG.Milestones.ct_even_small_lie_standard_frontier_models
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(hK : CFSG.Assembly.KProper CFSG.Blueprint.Catalog G)
(L : Subgroup G) (hL : standardComponentIsStandard L)
(hcore : ∀ t : G, orderOf t = 2 →
standardComponentOddCore (Subgroup.centralizer ({t} : Set G)) = ⊥)
(S : Sylow 2 (Subgroup.centralizer (L : Set G)))
(hS : IsCyclic (S : Subgroup (Subgroup.centralizer (L : Set G))))
(htype : Blueprint.Recognition.Exact.EvenStandardType (L ⧸ Subgroup.center L))
(hexc : ¬ Blueprint.Recognition.Exact.EvenStandardException (L ⧸ Subgroup.center L))
(hres : Blueprint.Recognition.Exact.EvenStandardResidual L)
(hbcd : Blueprint.Recognition.Exact.ResidualB L ∨ Blueprint.Recognition.Exact.ResidualC L ∨
Blueprint.Recognition.Exact.ResidualD L) :
Blueprint.Recognition.EvenSporadicOutcome G
The files of 2 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.rank_three_even.
TheoremCT_even_standard_residual_reduction#
The milestone module CFSG.Milestones.CT_even_standard_residual_reduction, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/CT_even_standard_residual_reduction.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.ct_even_standard_residual_reduction (theorem, line 1044). Proved here.
theorem _root_.CFSG.Milestones.ct_even_standard_residual_reduction
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(hK : CFSG.Assembly.KProper CFSG.Blueprint.Catalog G)
(L : Subgroup G) (hL : standardComponentIsStandard L)
(hcore : ∀ t : G, orderOf t = 2 →
standardComponentOddCore (Subgroup.centralizer ({t} : Set G)) = ⊥)
(S : Sylow 2 (Subgroup.centralizer (L : Set G)))
(hS : IsCyclic (S : Subgroup (Subgroup.centralizer (L : Set G))))
(htype : Blueprint.Recognition.Exact.EvenStandardType (L ⧸ Subgroup.center L))
(hexc : ¬ Blueprint.Recognition.Exact.EvenStandardException (L ⧸ Subgroup.center L)) :
Blueprint.Recognition.Exact.EvenStandardResidual L
The files of 2 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.rank_three_even.
TheoremCT_initial_standard_component_frontier#
The milestone module CFSG.Milestones.CT_initial_standard_component_frontier, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/CT_initial_standard_component_frontier.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.ct_initial_standard_component_frontier (theorem, line 16). Proved here.
theorem _root_.CFSG.Milestones.ct_initial_standard_component_frontier
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a) (hK : KProper CFSG.Blueprint.Catalog G)
(hrank : 3 ≤ twoRank G)
(hcomp : IsComponentType G) (hB : LocalBProperty G) :
(∃ t : G, orderOf t = 2 ∧ ∃ L : Subgroup G,
IsComponentOf L (Subgroup.centralizer ({t} : Set G)) ∧ IsStandardSubgroup L) ∨
(∃ z : G, orderOf z = 2 ∧ ∃ J : Subgroup G,
IsComponentOf J (Subgroup.centralizer ({z} : Set G)) ∧ z ∈ J ∧
∃ r : ℕ, 3 ≤ r ∧ ∃ S : Sylow 2 J,
Nonempty ((S : Subgroup J) ≃* QuaternionGroup (2 ^ (r - 2))))
The files of 2 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.rank_three_even.
Uses 4 · Used by 1
TheoremCT_odd_standard_recognition_frontier#
The milestone module CFSG.Milestones.CT_odd_standard_recognition_frontier, one of those CFSG/Milestones.lean imports.
It declares 2 results, quoted from CFSG/Milestones/CT_odd_standard_recognition_frontier.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.ct_odd_standard_recognition_frontier (theorem, line 3450). Proved here.
theorem _root_.CFSG.Milestones.ct_odd_standard_recognition_frontier
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(hK : CFSG.Assembly.KProper CFSG.Blueprint.Catalog G)
(L : Subgroup G) (hL : standardComponentIsStandard L)
(htype : Blueprint.Recognition.Exact.OddStandardType (L ⧸ Subgroup.center L)) :
(∃ n : ℕ, 9 ≤ n ∧ Nonempty (G ≃* alternatingGroup (Fin n))) ∨
(∃ p : ℕ, p.Prime ∧ p ≠ 2 ∧ Nat.card G ∈ lieOrdersChar p) ∨
Nat.card G ∈ standardComponentOddSporadicOrders
CFSG.Milestones.ct_odd_standard_recognition_frontier_models (theorem, line 3481). Proved here.
theorem _root_.CFSG.Milestones.ct_odd_standard_recognition_frontier_models
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(hK : CFSG.Assembly.KProper CFSG.Blueprint.Catalog G)
(L : Subgroup G) (hL : standardComponentIsStandard L)
(htype : Blueprint.Recognition.Exact.OddStandardType (L ⧸ Subgroup.center L)) :
(∃ n : ℕ, 9 ≤ n ∧ Nonempty (G ≃* alternatingGroup (Fin n))) ∨ Blueprint.OddLieType G ∨
(Blueprint.NativeSporadic.IsSporadic G .M12 ∨ Blueprint.NativeSporadic.IsSporadic G .J1 ∨
Blueprint.NativeSporadic.IsSporadic G .J2 ∨ Blueprint.NativeSporadic.IsSporadic G .HS ∨
Blueprint.NativeSporadic.IsSporadic G .McL ∨ Blueprint.NativeSporadic.IsSporadic G .Ly ∨
Blueprint.NativeSporadic.IsSporadic G .Suz ∨ Blueprint.NativeSporadic.IsSporadic G .He ∨
Blueprint.NativeSporadic.IsSporadic G .ONan)
The files of 2 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.rank_three_even.
TheoremCT_quaternion_component_recognition_frontier#
The milestone module CFSG.Milestones.CT_quaternion_component_recognition_frontier, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/CT_quaternion_component_recognition_frontier.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.ct_quaternion_component_recognition_frontier (theorem, line 1795). Proved here.
theorem _root_.CFSG.Milestones.ct_quaternion_component_recognition_frontier
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a) (hK : KProper InCatalog G)
(z : G) (hz : orderOf z = 2)
(J : Subgroup G) (hJ : IsComponentOf J (Subgroup.centralizer ({z} : Set G)))
(hzJ : z ∈ J) (S : Sylow 2 J)
(hS : ∃ r : ℕ, 3 ≤ r ∧ Nonempty ((S : Subgroup J) ≃* QuaternionGroup (2 ^ (r - 2)))) :
OddLieType G ∨ Nonempty (G ≃* M11)
The files of 2 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.rank_three_even.
Uses 1 · Used by 1
TheoremCT_rank_two_standard_recognition_frontier#
The milestone module CFSG.Milestones.CT_rank_two_standard_recognition_frontier, one of those CFSG/Milestones.lean imports.
It declares 2 results, quoted from CFSG/Milestones/CT_rank_two_standard_recognition_frontier.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.ct_rank_two_standard_recognition_frontier (theorem, line 917). Proved here.
theorem _root_.CFSG.Milestones.ct_rank_two_standard_recognition_frontier
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(hK : CFSG.Assembly.KProper CFSG.Blueprint.Catalog G)
(L : Subgroup G) (hL : standardComponentIsStandard L)
(hrank : 2 ≤ pRank 2 (Subgroup.centralizer (L : Set G))) :
(∃ n : ℕ, 9 ≤ n ∧ Nonempty (G ≃* alternatingGroup (Fin n))) ∨
Nat.card G ∈ standardComponentRankTwoSporadicOrders
CFSG.Milestones.ct_rank_two_standard_recognition_frontier_models (theorem, line 932). Proved here.
theorem _root_.CFSG.Milestones.ct_rank_two_standard_recognition_frontier_models
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a)
(hK : CFSG.Assembly.KProper CFSG.Blueprint.Catalog G)
(L : Subgroup G) (hL : standardComponentIsStandard L)
(hrank : 2 ≤ pRank 2 (Subgroup.centralizer (L : Set G))) :
(∃ n : ℕ, 9 ≤ n ∧ Nonempty (G ≃* alternatingGroup (Fin n))) ∨
(Blueprint.NativeSporadic.IsSporadic G .J2 ∨ Blueprint.NativeSporadic.IsSporadic G .Suz ∨
Blueprint.NativeSporadic.IsSporadic G .He ∨ Blueprint.NativeSporadic.IsSporadic G .Ru ∨
Blueprint.NativeSporadic.IsSporadic G .Co1)
The files of 2 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.rank_three_even.
Uses 9 · Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.