three_almost_prime_seventyfive
plain-language theorem explainer
75 factors as 3 times 5 squared and therefore satisfies Omega(75) equals three. Number theorists checking small cases of almost-prime predicates would reference this explicit instance. The proof reduces to a direct native computation of the big-Omega function at this argument.
Claim. $Omega(75)=3$, where $Omega(n)$ counts the 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 its big-Omega value equals three, as stated in the upstream definition: 'A number is 3-almost prime if Ω(n) = 3.' The local setting keeps statements minimal while the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the definition of isThreeAlmostPrime at 75.
why it matters
This concrete check populates the arithmetic-functions layer inside NumberTheory.Primes. It verifies a small case of the 3-almost-prime predicate but carries no dependence on the Recognition Science forcing chain, J-uniqueness, or the phi-ladder. No downstream results cite it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.