Counts of elements of each order
DefinitionShi's question on element-order counts (Kourovka 18.112)#✓fully proved
The proposition that if a finite group \(G\) has the property that, for every divisor \(d > 1\) of \(|G|\) and every subgroup \(H\) of \(G\) whose order is coprime to \(d\), \(|H|\) divides the number of elements of \(G\) of order \(d\), then every non-identity element of \(G\) has prime-power order.
def elementOrderCountPrimePowerOrders : Prop :=
∀ (G : Type) [Group G] [Finite G],
(∀ d : ℕ, 1 < d → d ∣ Nat.card G → ∀ H : Subgroup G, Nat.Coprime (Nat.card H) d →
Nat.card H ∣ Nat.card {g : G // orderOf g = d}) →
∀ g : G, g ≠ 1 → IsPrimePow (orderOf g)
Used by 1
TheoremCounting elements of each order forces prime-power orders#●ready to prove
Let \(G\) be a finite group such that for every divisor \(d > 1\) of \(|G|\) and every subgroup \(H\) of \(G\) whose order is coprime to \(d\), the order \(|H|\) divides the number of elements of \(G\) of order \(d\). Then every non-identity element of \(G\) has prime-power order.
Buturlakin, Shen and Shi proved this in 2017, answering Kourovka Problem 18.112 (W. J. Shi); the Kourovka Archive answers 18.112 "Yes, it is true".
public theorem_wanted elementOrderCountPrimePowerOrders_holds : elementOrderCountPrimePowerOrders
def elementOrderCountPrimePowerOrders : Prop :=
∀ (G : Type) [Group G] [Finite G],
(∀ d : ℕ, 1 < d → d ∣ Nat.card G → ∀ H : Subgroup G, Nat.Coprime (Nat.card H) d →
Nat.card H ∣ Nat.card {g : G // orderOf g = d}) →
∀ g : G, g ≠ 1 → IsPrimePow (orderOf g)
WantedExt/GroupTheory/ElementOrderCountPrimePowerKourovka18Problem112Wanted.lean:40
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 18.112 (W. J. Shi); resolution: A. A. Buturlakin, R. Shen and W. Shi, Siberian Math. J. 58 (2017), 405-407, Kourovka Archive, Problem 18.112 (Yes, it is true).
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.