Derived length of p-groups via 2-generator subgroups

DefinitionKourovka Problem 17.46, with the bound \(4\)#✓fully proved

The statement that for every prime \(p\) and every finite \(p\)-group \(G\) such that for all \(x, y \in G\) the derived subgroup \([H, H]\) of \(H = \langle x, y \rangle\) is cyclic, \(G\) has derived length at most \(4\), that is, the fourth term \(G^{(4)}\) of the derived series of \(G\) is trivial.

def twoGeneratorCyclicDerivedLengthAtMostFour : Prop :=
  ∀ (p : ℕ) (G : Type) [Group G] [Finite G], p.Prime → IsPGroup p G →
    (∀ x y : G, IsCyclic ↥⁅Subgroup.closure {x, y}, Subgroup.closure {x, y}⁆) →
      derivedSeries G 4 = ⊥

Used by 1

Used byDerived length of \(p\)-groups whose \(2\)-generator subgroups have cyclic derived subgroups (Kourovka Problem 17.46)

TheoremDerived length of \(p\)-groups whose \(2\)-generator subgroups have cyclic derived subgroups (Kourovka Problem 17.46)#●ready to prove

Derived length of \(p\)-groups whose \(2\)-generator subgroups have cyclic derived subgroups (Kourovka Problem 17.46). Let \(p\) be a prime and \(G\) a finite \(p\)-group such that for all \(x, y \in G\) the derived subgroup \([H, H]\) of \(H = \langle x, y \rangle\) is cyclic. Then \(G\) has derived length at most \(4\), that is, the fourth term \(G^{(4)}\) of the derived series of \(G\) is trivial.

public theorem_wanted twoGeneratorCyclicDerivedLengthAtMostFour_holds :
    twoGeneratorCyclicDerivedLengthAtMostFour

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 17.46 (B. M. Veretennikov); resolution: B. Wilkens, J. Group Theory 17 (2014), 151-174, Kourovka Archive, Problem 17.46 (Yes, it is at most 4).

Uses 1

Statement usesKourovka Problem 17.46, with the bound \(4\)

DefinitionMetacyclic group#✓fully proved

A group \(G\) is metacyclic if it has a cyclic normal subgroup \(N\) such that the quotient \(G/N\) is cyclic.

def IsMetacyclic (G : Type*) [Group G] : Prop :=
  ∃ N : Subgroup G, ∃ _ : N.Normal, IsCyclic N ∧ IsCyclic (G ⧸ N)

Used by 1

Used byKourovka Problem 15.33, with the bound \(2\)

DefinitionKourovka Problem 15.33, with the bound \(2\)#✓fully proved

The statement that every finite \(2\)-group \(G\) such that for all \(x, y \in G\) the subgroup \(\langle x, y \rangle\) generated by \(x\) and \(y\) is metacyclic has derived length at most \(2\), that is, its second derived subgroup \(G''\) is trivial.

def twoGeneratorMetacyclicMetabelian : Prop :=
  ∀ (G : Type) [Group G] [Finite G], IsPGroup 2 G →
    (∀ x y : G, IsMetacyclic (Subgroup.closure ({x, y} : Set G))) → derivedSeries G 2 = ⊥

Uses 1 · Used by 1

Statement usesMetacyclic group

Used byFinite \(2\)-groups with metacyclic \(2\)-generator subgroups are metabelian (Kourovka Problem 15.33)

TheoremFinite \(2\)-groups with metacyclic \(2\)-generator subgroups are metabelian (Kourovka Problem 15.33)#●ready to prove

Finite \(2\)-groups with metacyclic \(2\)-generator subgroups are metabelian (Kourovka Problem 15.33). Let \(G\) be a finite \(2\)-group such that for all \(x, y \in G\) the subgroup \(\langle x, y \rangle\) generated by \(x\) and \(y\) is metacyclic, that is, has a cyclic normal subgroup with cyclic quotient. Then \(G\) is metabelian: its second derived subgroup \(G''\) is trivial.

public theorem_wanted twoGeneratorMetacyclicMetabelian_holds : twoGeneratorMetacyclicMetabelian

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 15.33 (Ya. G. Berkovich); resolution: E. Crestani and F. Menegazzo, J. Group Theory 15 (2012), no. 3, 359-383, Kourovka Archive, Problem 15.33 (answer: Yes, it is at most 2).

Uses 1

Statement usesKourovka Problem 15.33, with the bound \(2\)

3 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.