Prime divisors of element orders in soluble groups

DefinitionLinear bound on the prime divisors of a finite soluble group (Kourovka 14.66)#✓fully proved

The statement, posed by A. Moretó, that there are natural numbers \(a\) and \(b\) such that for every finite soluble group \(G\) and every natural number \(m\), if the order of every element of \(G\) has at most \(m\) distinct prime divisors, then \(|G|\) has at most \(am + b\) distinct prime divisors.

Equivalently, \(|\pi(G)| \le a\,\nu(G) + b\) for every finite soluble group \(G\), where \(\pi(G)\) is the set of primes dividing \(|G|\) and \(\nu(G)\) is the largest number of distinct primes dividing the order of a single element of \(G\).

def solublePrimeCountLinearInElementPrimeCount : Prop :=
  ∃ a b : ℕ, ∀ (G : Type) [Group G] [Finite G], Group.IsSolvable G → ∀ m : ℕ,
    (∀ g : G, (orderOf g).primeFactors.card ≤ m) → (Nat.card G).primeFactors.card ≤ a * m + b

Used by 1

Used byFinite soluble groups satisfy a linear prime-divisor bound

TheoremFinite soluble groups satisfy a linear prime-divisor bound#●ready to prove

There are natural numbers \(a\) and \(b\) such that for every finite soluble group \(G\) and every natural number \(m\), if the order of every element of \(G\) has at most \(m\) distinct prime divisors, then \(|G|\) has at most \(am + b\) distinct prime divisors. That is, Kourovka Problem 14.66 has a positive answer.

Resolved true: the Kourovka Archive answers 14.66 "Yes, it does", citing Keller.

public theorem_wanted solublePrimeCountLinearInElementPrimeCount_holds :
    solublePrimeCountLinearInElementPrimeCount

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 14.66 (A. Moretó); resolution: T. M. Keller, J. Algebra 178 (1995), no. 2, 643-652, Kourovka Archive, Problem 14.66 (answer: Yes, it does).

Uses 1

Statement usesLinear bound on the prime divisors of a finite soluble group (Kourovka 14.66)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.