three_almost_prime_twenty
plain-language theorem explainer
The theorem confirms that 20 factors as 2 squared times 5 and therefore carries exactly three prime factors counted with multiplicity. Number theorists working with the total prime omega function or explicit checks of almost-prime predicates would reference this instance. The proof reduces to a single native_decide call that evaluates the bigOmega definition on the concrete input.
Claim. $Ω(20) = 3$, where $Ω(n)$ counts the total number of prime factors of $n$ with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. A number is declared 3-almost prime precisely when its total prime factor count with multiplicity equals three, via the definition isThreeAlmostPrime n := bigOmega n = 3. The present declaration supplies the explicit case n = 20, whose factorization 2² × 5 yields Ω(20) = 3.
proof idea
The proof is a one-line wrapper that applies native_decide to compute bigOmega 20 and confirm equality to 3.
why it matters
This concrete verification populates the arithmetic-functions layer that supports prime-related statements inside the Recognition framework. It instantiates the 3-almost-prime predicate for a small integer without new hypotheses or axioms. No downstream theorems are recorded, leaving open whether the instance will be invoked in later results on prime distributions or Möbius inversion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.