Highly composite numbers

DefinitionHighly composite numbers#✓fully proved

A positive natural number is highly composite if it has strictly more divisors than every smaller positive natural number.

def IsHighlyComposite (H : ℕ) : Prop :=
  0 < H ∧ ∀ m : ℕ, 0 < m → m < H → m.divisors.card < H.divisors.card

Used by 2

Used byPrime divisors of highly composite numbers form an initial segment · Exponents of highly composite numbers are non-increasing

TheoremExponents of highly composite numbers are non-increasing#✓fully proved

If \(H\) is a highly composite number and \(p \le q\) are primes, then the exponent of \(q\) in the prime factorization of \(H\) is at most the exponent of \(p\).

theorem IsHighlyComposite.factorization_antitone {H p q : ℕ}
    (hH : H.IsHighlyComposite) (hp : p.Prime) (hq : q.Prime) (hpq : p ≤ q) :
    H.factorization q ≤ H.factorization p

Uses 1 · Used by 1

Statement usesHighly composite numbers

Used byPrime divisors of highly composite numbers form an initial segment

TheoremPrime divisors of highly composite numbers form an initial segment#✓fully proved

If \(H\) is a highly composite number and \(p \le q\) are primes with \(q \mid H\), then \(p \mid H\). In other words, the set of primes dividing \(H\) is an initial segment of the primes.

theorem IsHighlyComposite.dvd_of_prime_le {H p q : ℕ}
    (hH : H.IsHighlyComposite) (hp : p.Prime) (hq : q.Prime)
    (hpq : p ≤ q) (hqH : q ∣ H) : p ∣ H

Uses 2

Statement usesHighly composite numbers

Proof usesExponents of highly composite numbers are non-increasing

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.