Almost prime numbers

This file defines Nat.IsAlmostPrime k n, the predicate that n has exactly k prime factors counted with multiplicity. We also define Nat.IsAtMostAlmostPrime, the corresponding predicate with at most k prime factors, and Nat.IsSemiprime, the special case of 2-almost-prime numbers.

Both definitions use the arithmetic function ArithmeticFunction.cardFactors, written Ω.

The terminology follows the standard definition of an almost prime.

Main statements

• Nat.IsAlmostPrime.mul: the product of a k-almost-prime number and an l-almost-prime number is (k + l)-almost-prime.
• Nat.IsAtMostAlmostPrime.mul: the analogous statement for at most k prime factors.

def Nat.IsAlmostPrime (k n : ℕ) : Prop

IsAlmostPrime k n means that n is k-almost prime: it has exactly k prime factors, counted with multiplicity. The side condition excludes 0, so 1 is 0-almost prime.

Equations

• k.IsAlmostPrime n = (n ≠ 0 ∧ ArithmeticFunction.cardFactors n = k)

def Nat.IsAtMostAlmostPrime (k n : ℕ) : Prop

IsAtMostAlmostPrime k n means that n has at most k prime factors, counted with multiplicity.

Equations

• k.IsAtMostAlmostPrime n = (n ≠ 0 ∧ ArithmeticFunction.cardFactors n ≤ k)

@[reducible, inline]

abbrev Nat.IsSemiprime (n : ℕ) : Prop

A semiprime is a 2-almost-prime number.

Equations

• n.IsSemiprime = Nat.IsAlmostPrime 2 n

@[simp]

theorem Nat.isAlmostPrime_zero_iff {n : ℕ} : IsAlmostPrime 0 n ↔ n = 1

@[simp]

theorem Nat.isAlmostPrime_one_iff {n : ℕ} : IsAlmostPrime 1 n ↔ Prime n

theorem Nat.Prime.isAlmostPrime_one {p : ℕ} (hp : Prime p) : IsAlmostPrime 1 p

theorem Nat.IsAlmostPrime.mul {k l m n : ℕ} (hm : k.IsAlmostPrime m) (hn : l.IsAlmostPrime n) : (k + l).IsAlmostPrime (m * n)

theorem Nat.IsAtMostAlmostPrime.mul {k l m n : ℕ} (hm : k.IsAtMostAlmostPrime m) (hn : l.IsAtMostAlmostPrime n) : (k + l).IsAtMostAlmostPrime (m * n)

theorem Nat.IsAlmostPrime.isAtMost {k l n : ℕ} (hn : k.IsAlmostPrime n) (hkl : k ≤ l) : l.IsAtMostAlmostPrime n

theorem Nat.Prime.mul_isAlmostPrime_two {p q : ℕ} (hp : Prime p) (hq : Prime q) : IsAlmostPrime 2 (p * q)

theorem Nat.Prime.sq_isAlmostPrime_two {p : ℕ} (hp : Prime p) : IsAlmostPrime 2 (p ^ 2)