omega_apply
plain-language theorem explainer
The declaration equates the distinct-prime-factor counting function omega(n) to the length of the deduplicated prime-factors list of n. Analytic number theorists cite the equivalence when reducing omega expressions to explicit factorizations. The proof is a one-line term simplification that unfolds the definition of omega and applies the cardDistinctFactors_apply lemma.
Claim. For every natural number $n$, $ω(n)$ equals the length of the deduplicated list of prime factors of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to omega and bigOmega. omega counts the number of distinct prime factors of its argument and is realized as the arithmetic function cardDistinctFactors. The local setting keeps statements minimal so that Dirichlet inversion and related algebra can be added once the basic interfaces stabilize.
proof idea
The proof is a term-mode simplification. It rewrites omega by its definition and applies ArithmeticFunction.cardDistinctFactors_apply to obtain the length of the deduplicated prime-factors list.
why it matters
The equivalence is invoked by the downstream theorem omega_one, which concludes that omega(1) equals zero. It supplies a basic interface in the arithmetic-functions module, supporting prime-counting calculations that appear in later Recognition Science developments such as mass formulas on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.