omega
plain-language theorem explainer
omega is the standard arithmetic function that counts the distinct prime divisors of a natural number n. Number theorists working with prime factorizations or Möbius inversion cite it when they need the unweighted prime-counting map. The declaration is a one-line abbreviation that directly re-exports Mathlib's cardDistinctFactors under the conventional name omega.
Claim. Let $n$ be a natural number. The function $omega(n)$ equals the number of distinct prime divisors of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. These wrappers prepare the ground for Dirichlet inversion and square-free detection without yet entering full Dirichlet algebra. omega is introduced alongside bigOmega and the various Möbius lemmas that appear as siblings.
proof idea
The declaration is a direct abbreviation that aliases ArithmeticFunction.cardDistinctFactors to the identifier omega.
why it matters
It supplies the conventional ω function required for any later arithmetic-function identities inside the primes module. The surrounding file positions these definitions as footholds for Möbius-based arguments; omega is the unweighted counterpart to the multiplicity-aware bigOmega.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.