Recognition of PSL(2, 7) by spectrum
DefinitionKourovka Problem 16.57: recognition of PSL(2, 7) by spectrum#✓fully proved
The statement that every group \(G\), finite or infinite, whose set of element orders \(\{\operatorname{ord}(g) : g \in G\}\) equals \(\{1, 2, 3, 4, 7\}\) is isomorphic to \(L_2(7) = \mathrm{PSL}(2, 7)\), the projective special linear group of \(2 \times 2\) matrices over the field \(\mathbb{Z}/7\mathbb{Z}\).
def spectrumRecognizesPSL27 : Prop :=
∀ (G : Type) [Group G], Set.range (orderOf : G → ℕ) = {1, 2, 3, 4, 7} →
Nonempty (G ≃* Matrix.ProjectiveSpecialLinearGroup (Fin 2) (ZMod 7))Used by 1
TheoremLytkina–Kuznetsov theorem: PSL(2, 7) is recognizable by spectrum#●ready to prove
Every group \(G\), finite or infinite, whose set of element orders \(\{\operatorname{ord}(g) : g \in G\}\) equals \(\{1, 2, 3, 4, 7\}\) is isomorphic to \(L_2(7) = \mathrm{PSL}(2, 7)\), the projective special linear group of \(2 \times 2\) matrices over the field \(\mathbb{Z}/7\mathbb{Z}\).
public theorem_wanted spectrumRecognizesPSL27_holds : spectrumRecognizesPSL27def spectrumRecognizesPSL27 : Prop :=
∀ (G : Type) [Group G], Set.range (orderOf : G → ℕ) = {1, 2, 3, 4, 7} →
Nonempty (G ≃* Matrix.ProjectiveSpecialLinearGroup (Fin 2) (ZMod 7))WantedExt/GroupTheory/SpectrumRecognitionPSL27Kourovka16Problem57Wanted.lean:37
Sources
- E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Archive of Solved Problems, Problem 16.57 (V. D. Mazurov); resolution: D. V. Lytkina and A. A. Kuznetsov, Sib. Èlektron. Mat. Izv. 4 (2007), 136-140, Kourovka Archive, Problem 16.57 (Yes, it is).
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.