omega_onehundredtwenty
plain-language theorem explainer
The theorem asserts that the arithmetic function counting distinct prime factors evaluates to exactly 3 at the integer 120. Number theorists checking small cases in factorization or Möbius inversion setups would reference this concrete value. The proof is a direct one-line evaluation that applies native_decide to the definition.
Claim. $ω(120) = 3$, where $ω(n)$ denotes the number of 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 omega. Omega here records the count of distinct primes, separate from the total multiplicity function Ω. The local setting keeps statements minimal to allow later layering of Dirichlet algebra and inversion once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to evaluate the arithmetic function definition directly on the concrete integer 120.
why it matters
This supplies a concrete verification point inside the arithmetic functions section. It anchors small-case checks on prime factorization counts before any move to inversion formulas or Dirichlet series. No parent theorems or open questions are attached in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.