three_almost_prime_twentyseven
plain-language theorem explainer
27 equals 3 cubed and therefore satisfies the condition that its total number of prime factors counted with multiplicity equals three. Number theorists checking small cases inside the arithmetic functions library would cite this result. The proof reduces to a direct native computation of the bigOmega predicate.
Claim. $27=3^3$ and therefore satisfies $Ω(27)=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 3-almost prime precisely when $Ω(n)=3$, as defined by the sibling declaration isThreeAlmostPrime n := bigOmega n = 3. The local setting is a collection of small verification statements that can later support Dirichlet inversion once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the boolean equality bigOmega 27 = 3.
why it matters
The declaration supplies a basic verification inside the arithmetic functions file. It supports the primes module by confirming a concrete instance of the 3-almost-prime predicate and aligns with the module's stated goal of keeping statements lightweight ahead of deeper algebraic work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.