CT_standard_recognition_assembly to LC_GL_embedding_theorem_D2_rank_…
TheoremCT_standard_recognition_assembly#
The milestone module CFSG.Milestones.CT_standard_recognition_assembly, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/CT_standard_recognition_assembly.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.ct_standard_recognition_assembly (theorem, line 3405). Proved here.
theorem _root_.CFSG.Milestones.ct_standard_recognition_assembly
(G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a) (hK : KProper InCatalog G)
(L : Subgroup G) (hL : IsStandardSubgroup L) : InCatalog G
The files of 2 case theorems import it, directly or through other files: CFSG.Assembly.component_type, CFSG.Assembly.rank_three_even.
Uses 2 · Used by 1
TheoremFAM_M_finiteness#
The milestone module CFSG.Milestones.FAM_M_finiteness, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/FAM_M_finiteness.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.fam_m_finiteness (theorem, line 13). Proved here.
theorem _root_.CFSG.Milestones.fam_m_finiteness :
Nat.card MonsterY443Derived = monsterOrder
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 3 · Used by 5
TheoremFAM_M_simplicity#
The milestone module CFSG.Milestones.FAM_M_simplicity, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/FAM_M_simplicity.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.fam_m_simplicity (theorem, line 13). Proved here.
theorem _root_.CFSG.Milestones.fam_m_simplicity :
IsSimpleGroup MonsterY443Derived
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.
TheoremFAM_Th_simplicity#
The milestone module CFSG.Milestones.FAM_Th_simplicity, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/FAM_Th_simplicity.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.fam_th_simplicity (theorem, line 10). Proved here.
theorem fam_th_simplicity :
IsSimpleGroup Blueprint.NativeSporadic.Th
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.
TheoremFAM_classical_model_membership#
The milestone module CFSG.Milestones.FAM_classical_model_membership, one of those CFSG/Milestones.lean imports.
It declares 4 results, quoted from CFSG/Milestones/FAM_classical_model_membership.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.ClassicalRep (def, line 12). A definition.
def ClassicalRep (G : Type) [Group G] : Prop
CFSG.Milestones.fam_classical_model_membership_alltags (theorem, line 16). Proved here.
theorem fam_classical_model_membership_alltags (G : Type) [Group G] :
ClassicalRep G ↔ ∃ (t : Assembly.LowTwoRank.StatedLieTag) (n p f : ℕ),
Assembly.LowTwoRank.StatedClassicalModel G t n p f
CFSG.Milestones.statedClassicalModel_tag_mem (theorem, line 20). Proved here.
theorem statedClassicalModel_tag_mem (G : Type) [Group G]
(t : Assembly.LowTwoRank.StatedLieTag) (n p f : ℕ)
(h : Assembly.LowTwoRank.StatedClassicalModel G t n p f) :
t ∈ ({.PSL, .PSU, .PSp, .POmegaOdd, .POmegaPlus, .POmegaMinus} :
Set Assembly.LowTwoRank.StatedLieTag)
CFSG.Milestones.fam_classical_model_membership (theorem, line 35). Proved here.
theorem fam_classical_model_membership (G : Type) [Group G] :
ClassicalRep G ↔ ∃ t : Assembly.LowTwoRank.StatedLieTag,
t ∈ ({.PSL, .PSU, .PSp, .POmegaOdd, .POmegaPlus, .POmegaMinus} :
Set Assembly.LowTwoRank.StatedLieTag) ∧
∃ n p f : ℕ, Assembly.LowTwoRank.StatedClassicalModel G t n p f
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 13
TheoremFAM_sporadic_converse#
The milestone module CFSG.Milestones.FAM_sporadic_converse, one of those CFSG/Milestones.lean imports.
It declares 2 results, quoted from CFSG/Milestones/FAM_sporadic_converse.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.fam_sporadic_converse_tauCeti (theorem, line 14). Proved here.
theorem _root_.CFSG.Milestones.fam_sporadic_converse_tauCeti
(s : TauCeti.SporadicName) :
Finite s.Group ∧ IsSimpleGroup s.Group
CFSG.Milestones.fam_sporadic_converse (theorem, line 24). Proved here.
theorem fam_sporadic_converse
(G : Type) [Group G]
(hrep : Blueprint.NativeSporadic.SporadicRep G) : Finite G ∧ IsSimpleGroup G
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 2 · Used by 10
TheoremFAM_sporadic_finiteness#
The milestone module CFSG.Milestones.FAM_sporadic_finiteness, one of those CFSG/Milestones.lean imports.
It declares 2 results, quoted from CFSG/Milestones/FAM_sporadic_finiteness.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.fam_sporadic_finiteness_tauCeti (theorem, line 11). Proved here.
theorem fam_sporadic_finiteness_tauCeti
(G : Type) [Group G]
(hrep : ∃ s : TauCeti.SporadicName, Nonempty (G ≃* s.Group)) : Finite G
CFSG.Milestones.fam_sporadic_finiteness (theorem, line 26). Proved here.
theorem fam_sporadic_finiteness
(G : Type) [Group G]
(hrep : Blueprint.NativeSporadic.SporadicRep G) : Finite G
No case theorem's file imports it, directly or through other files.
Uses 1
TheoremFAM_sporadic_native_converse#
The milestone module CFSG.Milestones.FAM_sporadic_native_converse, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/FAM_sporadic_native_converse.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.fam_sporadic_native_converse (theorem, line 10). Proved here.
theorem fam_sporadic_native_converse
(G : Type) [Group G] (hrep : NativeSporadicRep G) :
Finite G ∧ Nontrivial G ∧ IsSimpleGroup G
No case theorem's file imports it, directly or through other files.
Uses 1 · Used by 1
TheoremFAM_sporadic_representatives#
The milestone module CFSG.Milestones.FAM_sporadic_representatives, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/FAM_sporadic_representatives.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.fam_sporadic_representatives_definition (theorem, line 9). Proved here.
theorem fam_sporadic_representatives_definition (G : Type) [Group G] :
Blueprint.NativeSporadic.SporadicRep G ↔
∃ s : TauCeti.SporadicName, Nonempty (G ≃* Blueprint.NativeSporadic.Carrier s)
No case theorem's file imports it, directly or through other files.
TheoremFROB_kernel_existence#
The milestone module CFSG.Milestones.FROB_kernel_existence, one of those CFSG/Milestones.lean imports.
It declares 2 results, quoted from CFSG/Milestones/FROB_kernel_existence.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.frobenius_kernel (theorem, line 11). Proved here.
theorem _root_.CFSG.Milestones.frobenius_kernel (G X : Type) [Group G] [Fintype G] [Fintype X]
[MulAction G X] [FaithfulSMul G X]
(hcard : 2 ≤ Fintype.card X)
(htrans : ∀ x y : X, ∃ g : G, g • x = y)
(hstab : ∀ x : X, MulAction.stabilizer G x ≠ ⊥)
(hfrob : ∀ g : G, g ≠ 1 → ∀ x y : X, g • x = x → g • y = y → x = y) :
∃ N : Subgroup G, N.Normal ∧
(N : Set G) = {1} ∪ {g : G | ∀ x : X, g • x ≠ x}
CFSG.Milestones.frobenius_kernel_existence (theorem, line 26). Proved here.
theorem _root_.CFSG.Milestones.frobenius_kernel_existence {G : Type} [Group G] [Finite G] (H : Subgroup G)
(hH1 : H ≠ ⊥) (hHG : H ≠ ⊤)
(hfrob : ∀ g : G, g ∉ H → H ⊓ (MulAut.conj g • H) = ⊥) :
∃ K : Subgroup G,
(K : Set G) = {1} ∪ (Set.univ \ ⋃ g : G, ((MulAut.conj g • H : Subgroup G) : Set G)) ∧
K.Normal ∧ (∀ x : G, ∃ k ∈ K, ∃ h ∈ H, x = k * h) ∧ K ⊓ H = ⊥ ∧
Nat.card K = H.index
No case theorem's file imports it, directly or through other files.
TheoremGW_original_maximal_odd_S_invariant_R_and_normalizer_core#
The milestone module CFSG.Milestones.GW_original_maximal_odd_S_invariant_R_and_normalizer_core, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/GW_original_maximal_odd_S_invariant_R_and_normalizer_core.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.gw_original_maximal_odd_s_invariant_r_and_normalizer_core (theorem, line 11). Proved here.
theorem gw_original_maximal_odd_s_invariant_r_and_normalizer_core (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a) (d : OriginalData G)
(hs : d.Stationarity) (hc : d.CanonicalNormalizers) : d.MaximalOddKernel
No case theorem's file imports it, directly or through other files.
TheoremGW_original_normalizer_R_pure_projective_shared_fourgroup_and_index_divisor#
The milestone module CFSG.Milestones.GW_original_normalizer_R_pure_projective_shared_fourgroup_and_index_divisor, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/GW_original_normalizer_R_pure_projective_shared_fourgroup_and_index_divisor.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.gw_original_normalizer_r_pure_projective_shared_fourgroup_and_index_divisor (theorem, line 14). Proved here.
theorem gw_original_normalizer_r_pure_projective_shared_fourgroup_and_index_divisor (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a) (d : OriginalData G)
(hs : d.Stationarity) (hc : d.CanonicalNormalizers) (hm : d.MaximalOddKernel)
(hR : d.R ≠ ⊥) (hCN : d.C < d.N) : d.PureProjectiveNormalizer
No case theorem's file imports it, directly or through other files.
Sources
Uses 1
TheoremGW_original_normalizer_coset_involution_fixedpoints_secondary_torus_divisibility#
The milestone module CFSG.Milestones.GW_original_normalizer_coset_involution_fixedpoints_secondary_torus_divisibility, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/GW_original_normalizer_coset_involution_fixedpoints_secondary_torus_divisibility.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.gw_original_normalizer_coset_involution_fixedpoints_secondary_torus_divisibility (theorem, line 12). Proved here.
theorem gw_original_normalizer_coset_involution_fixedpoints_secondary_torus_divisibility (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a) (d : OriginalData G)
(hs : d.Stationarity) (hc : d.CanonicalNormalizers) (hm : d.MaximalOddKernel)
(hp : d.PureProjectiveNormalizer) (hR : d.R ≠ ⊥) (hCN : d.C < d.N) : d.CosetBounds
No case theorem's file imports it, directly or through other files.
TheoremGW_original_post_proposition_sixteen_all_prime_stationarity_and_no_growth#
The milestone module CFSG.Milestones.GW_original_post_proposition_sixteen_all_prime_stationarity_and_no_growth, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/GW_original_post_proposition_sixteen_all_prime_stationarity_and_no_growth.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.gw_original_post_proposition_sixteen_all_prime_stationarity_and_no_growth (theorem, line 13). Proved here.
theorem gw_original_post_proposition_sixteen_all_prime_stationarity_and_no_growth (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a) (d : OriginalData G)
: d.Stationarity
No case theorem's file imports it, directly or through other files.
Sources
Uses 2
TheoremGW_original_post_proposition_sixteen_canonical_stationary_prime_normalizers#
The milestone module CFSG.Milestones.GW_original_post_proposition_sixteen_canonical_stationary_prime_normalizers, one of those CFSG/Milestones.lean imports.
It declares 2 results, quoted from CFSG/Milestones/GW_original_post_proposition_sixteen_canonical_stationary_prime_normalizers.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.gw_original_post_proposition_sixteen_canonical_stationary_prime_normalizers (theorem, line 11). Proved here.
theorem gw_original_post_proposition_sixteen_canonical_stationary_prime_normalizers (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a) (d : OriginalData G)
(hs : d.Stationarity) : d.CanonicalNormalizers
CFSG.Milestones.gw_original_post_proposition_sixteen_canonical_stationary_prime_normalizers_full (theorem, line 22). Proved here.
theorem gw_original_post_proposition_sixteen_canonical_stationary_prime_normalizers_full (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a) (d : OriginalData G)
(hs : d.Stationarity) : d.CanonicalNormalizersFull
No case theorem's file imports it, directly or through other files.
Sources
Uses 1
TheoremGW_original_q_five_index_three_character_kernel_order_contradiction#
The milestone module CFSG.Milestones.GW_original_q_five_index_three_character_kernel_order_contradiction, one of those CFSG/Milestones.lean imports.
It declares 2 results, quoted from CFSG/Milestones/GW_original_q_five_index_three_character_kernel_order_contradiction.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.gw_original_q_five_index_three_character_kernel_order_contradiction (theorem, line 12). Proved here.
theorem gw_original_q_five_index_three_character_kernel_order_contradiction (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a) (d : OriginalData G)
(hs : d.Stationarity) (hc : d.CanonicalNormalizers) (hm : d.MaximalOddKernel)
(hp : d.PureProjectiveNormalizer) (hb : d.CosetBounds)
(hn : d.n = 3) (hR : d.R ≠ ⊥) (hCN : d.C < d.N)
(w : CoordinateWitness (d.N ⧸ CFSG.Assembly.oddCore d.N)) (hq : Nat.card w.K = 5)
(hindex : (d.commonE.subgroupOf d.R).index = 3) (horder : d.ConditionalOrder) : d.CharacterKernelConclusion
CFSG.Milestones.gw_original_q_five_index_three_character_kernel_order_contradiction_full (theorem, line 28). Proved here.
theorem gw_original_q_five_index_three_character_kernel_order_contradiction_full (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
(hnonab : ∃ a b : G, a * b ≠ b * a) (d : OriginalData G)
(hs : d.Stationarity) (hc : d.CanonicalNormalizers) (hm : d.MaximalOddKernel)
(hp : d.PureProjectiveNormalizer) (hb : d.CosetBounds)
(hn : d.n = 3) (hR : d.R ≠ ⊥) (hCN : d.C < d.N)
(w : CoordinateWitness (d.N ⧸ CFSG.Assembly.oddCore d.N)) (hq : Nat.card w.K = 5)
(hindex : (d.commonE.subgroupOf d.R).index = 3) (horder : d.ConditionalOrderFull) : d.CharacterKernelConclusion
No case theorem's file imports it, directly or through other files.
TheoremLC_GL_GF2_recognition_rank_four#
The milestone module CFSG.Milestones.LC_GL_GF2_recognition_rank_four, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/LC_GL_GF2_recognition_rank_four.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.lc_gl_gf2_recognition_rank_four (theorem, line 2167). Proved here.
theorem _root_.CFSG.Milestones.lc_gl_gf2_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) (hgf2 : LargeEvenGF2Type G) : InCatalog G
The files of 1 case theorem import it, directly or through other files: CFSG.Assembly.large_even.
Uses 2 · Used by 1
TheoremLC_GL_constructed_pretrichotomy_rank_four#
The milestone module CFSG.Milestones.LC_GL_constructed_pretrichotomy_rank_four, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/LC_GL_constructed_pretrichotomy_rank_four.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.lc_gl_constructed_pretrichotomy_rank_four (theorem, line 1941). Proved here.
theorem _root_.CFSG.Milestones.lc_gl_constructed_pretrichotomy_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) ∨ LargeEvenGF2Type G ∨
∃ p ∈ LargeEvenBeta 4 G, ∃ (B : Subgroup G) (x : G) (L : Subgroup G),
LargeEvenSStar p B x L ∧ LargeEvenStandardType p B x L
The files of 1 case theorem import it, directly or through other files: CFSG.Assembly.large_even.
Uses 1 · Used by 1
TheoremLC_GL_embedding_theorem_D1_rank_four#
The milestone module CFSG.Milestones.LC_GL_embedding_theorem_D1_rank_four, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/LC_GL_embedding_theorem_D1_rank_four.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.lc_gl_embedding_theorem_d1_rank_four (theorem, line 12). Proved here.
theorem _root_.CFSG.Milestones.lc_gl_embedding_theorem_d1_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)
(p : ℕ) (hp : p ∈ GLBBetaFour G) (P : Sylow p G)
(M : Subgroup G) (hM : GLBIsMaxTwoLocal M) (hWM : GLBWeakCore p (P : Subgroup G) ≤ M)
(H : Subgroup G) (hH : IsTwoLocal H) (hHM : 3 ≤ pRank p (H ⊓ M)) :
H ≤ M
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 1
TheoremLC_GL_embedding_theorem_D2_rank_four#
The milestone module CFSG.Milestones.LC_GL_embedding_theorem_D2_rank_four, one of those CFSG/Milestones.lean imports.
It declares 1 result, quoted from CFSG/Milestones/LC_GL_embedding_theorem_D2_rank_four.lean in AxiomMath/CFSG at commit 69cb972f, Apache-2.0:
CFSG.Milestones.lc_gl_embedding_theorem_d2_rank_four (theorem, line 12). Proved here.
theorem _root_.CFSG.Milestones.lc_gl_embedding_theorem_d2_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)
(hδ₁ : GLBDeltaOne G) (hδ₂ : GLBDeltaTwo G)
(p : ℕ) (hp : p ∈ GLBBetaFour G) (P : Sylow p G)
(M : Subgroup G) (hM : GLBIsMaxTwoLocal M) (hPM : GLBCore p 2 (P : Subgroup G) ≤ M)
(Q : Subgroup G) (hQ : IsPGroup p Q) (hQrank : pRank p Q = 2) (hQM : GLBCore p 1 Q ≤ M)
(H : Subgroup G) (hH : IsTwoLocal H) (hQH : Q ≤ H) :
H ≤ M
The files of 2 case theorems import it, directly or through other files: CFSG.Assembly.rank_three_even, CFSG.Assembly.large_even.
Uses 1 · Used by 2
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.