omega_one
plain-language theorem explainer
The distinct prime factor counting function ω evaluates to zero at the unit. Number theorists applying arithmetic functions in Dirichlet series or inversion formulas would cite this base case for consistency at n=1. The proof reduces immediately to the explicit definition of ω via a single simplification step.
Claim. $ω(1) = 0$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to related maps such as ω. The upstream result states that ω(n) equals the length of the deduplicated list of prime factors of n. This places the declaration inside the standard setup of multiplicative arithmetic functions, where evaluation at the unit serves as the starting point for convolution identities.
proof idea
One-line wrapper that applies the definition of ω and simplifies the empty prime-factors list at n=1.
why it matters
The result anchors the ω function at the multiplicative identity, a prerequisite for any subsequent arithmetic-function algebra in the NumberTheory.Primes module. It supplies the necessary base case before Möbius inversion or square-free characterizations are layered on. No downstream citations appear yet, but the declaration closes the unit evaluation required for the function to be well-defined on all natural numbers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.