Recognition by order and spectrum

DefinitionSet of element orders (Kourovka 12.39)#✓fully proved

For a group \(G\), the set of natural numbers that occur as the order of some element of \(G\), where an element of infinite order is counted as having order \(0\).

def elementOrders (G : Type*) [Group G] : Set ℕ :=
  Set.range (orderOf : G → ℕ)

Used by 1

Used byShi's conjecture on recognition by order and element orders (Kourovka 12.39)

DefinitionShi's conjecture on recognition by order and element orders (Kourovka 12.39)#✓fully proved

The statement that for every finite group \(G\) and every finite simple group \(S\), if \(G\) and \(S\) have the same order and the same set of element orders, then \(G\) is isomorphic to \(S\).

def simpleGroupRecognizedByOrderAndSpectrum : Prop :=
  ∀ (G S : Type) [Group G] [Finite G] [Group S] [Finite S], IsSimpleGroup S →
    Nat.card G = Nat.card S → elementOrders G = elementOrders S → Nonempty (G ≃* S)

Uses 1 · Used by 1

Statement usesSet of element orders (Kourovka 12.39)

Used byFinite simple groups are recognized by order and element orders

TheoremFinite simple groups are recognized by order and element orders#●ready to prove

For every finite group \(G\) and every finite simple group \(S\), if \(G\) and \(S\) have the same order and the same set of element orders, then \(G\) is isomorphic to \(S\). That is, Shi's conjecture (Kourovka Problem 12.39) holds.

Here a simple group may be cyclic of prime order. The Kourovka Archive records the answer "Yes, they must", proved by Xu and Shi and by Vasil'ev, Grechkoseeva and Mazurov.

public theorem_wanted simpleGroupRecognizedByOrderAndSpectrum_holds :
    simpleGroupRecognizedByOrderAndSpectrum

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 12.39 (W. J. Shi; A. S. Kondratiev); resolution: M. C. Xu and W. J. Shi, Algebra Colloq. 10 (2003), 427-443; A. V. Vasil'ev, M. A. Grechkoseeva and V. D. Mazurov, Algebra Logic 48 (2009), 385-409, Kourovka Archive, Problem 12.39: Yes, they must.

Uses 1

Statement usesShi's conjecture on recognition by order and element orders (Kourovka 12.39)

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.