five_almost_prime_onehundredeighty
plain-language theorem explainer
The declaration verifies that 180 has total prime factor count five under the bigOmega function. Number theorists building tables of almost-prime examples or testing arithmetic function wrappers would cite this concrete case. The proof reduces to a single native_decide call that evaluates the definition directly on the input.
Claim. $180 = 2^2 3^2 5$ implies $Omega(180) = 5$, where $Omega(n)$ counts all prime factors of $n$ with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to bigOmega. The predicate isFiveAlmostPrime is defined by the equation bigOmega n = 5. This places the theorem inside a collection of small verification statements that stabilize basic interfaces before deeper Dirichlet algebra is added.
proof idea
One-line wrapper that applies the native_decide tactic to the definition of isFiveAlmostPrime.
why it matters
The result supplies a verified concrete instance inside the arithmetic-functions scaffolding of the NumberTheory.Primes library. It supports any later work that enumerates almost-primes or applies the bigOmega predicate, consistent with the module's goal of providing stable footholds around Mathlib definitions. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.