Generating p-groups by elements of equal order

DefinitionGenerating sets of equal order in finite p-groups (Kourovka 11.6)#✓fully proved

The statement that for every odd prime \(p\), every finite \(p\)-group \(G\) has a generating set \(S\) all of whose elements have the same order.

def pGroupEqualOrderGenerators : Prop :=
  ∀ p : ℕ, p.Prime → Odd p → ∀ (G : Type) [Group G] [Finite G], IsPGroup p G →
    ∃ S : Set G, Subgroup.closure S = ⊤ ∧ ∃ m : ℕ, ∀ x ∈ S, orderOf x = m

Used by 1

Used byFinite p-groups without a generating set of elements of equal order

TheoremFinite p-groups without a generating set of elements of equal order#●ready to prove

For some odd prime \(p\) there is a finite \(p\)-group \(G\) such that no generating set of \(G\) consists of elements that all have the same order. This answers Kourovka Problem 11.6 (Bagiński) in the negative (O'Brien, Scoppola and Vaughan-Lee).

public theorem_wanted pGroupEqualOrderGenerators_refuted : ¬ pGroupEqualOrderGenerators

def pGroupEqualOrderGenerators : Prop :=
  ∀ p : ℕ, p.Prime → Odd p → ∀ (G : Type) [Group G] [Finite G], IsPGroup p G →
    ∃ S : Set G, Subgroup.closure S = ⊤ ∧ ∃ m : ℕ, ∀ x ∈ S, orderOf x = m

WantedExt/GroupTheory/PGroupEqualOrderGeneratorsKourovka11Problem6Wanted.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 11.6 (C. Bagiński); resolution: E. A. O'Brien, C. M. Scoppola and M. R. Vaughan-Lee, Proc. Amer. Math. Soc. 134, no. 12 (2006), 3457-3464, Kourovka Archive, Problem 11.6: "No, it is not true", https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesGenerating sets of equal order in finite p-groups (Kourovka 11.6)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.