omega_six
plain-language theorem explainer
The declaration establishes that the arithmetic function ω evaluates to 2 at the input 6, matching the two distinct prime factors 2 and 3. Number theorists building Möbius inversion or prime-counting identities would cite this base evaluation. The proof is a one-line term that applies native_decide to compute the value directly from the imported definition.
Claim. $ω(6) = 2$, where $ω(n)$ counts the distinct prime factors of the positive integer $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to related maps such as bigOmega. Here omega is the standard little-omega function that returns the number of distinct primes dividing its argument, as shown by the sibling declarations for square-free predicates and bigOmega. The local setting keeps statements minimal so that Dirichlet convolution and inversion can be added once the basic interfaces are stable.
proof idea
The proof is a one-line term that invokes native_decide to evaluate omega at 6 by direct computation from the definition.
why it matters
This evaluation supplies a concrete checkpoint inside the arithmetic-functions scaffolding that supports Möbius-based arguments in the NumberTheory.Primes section. It aligns with the need for exact prime-factor counts when the Recognition framework later invokes arithmetic identities, even though no downstream theorem currently records a use of this specific fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.