omega_threehundredsixty
plain-language theorem explainer
The theorem asserts that the number of distinct prime factors of 360 equals three, matching the primes 2, 3 and 5. Number theorists consulting small-case values of arithmetic functions would cite this result for verification. The proof is a direct native_decide evaluation of the omega definition with no intermediate lemmas.
Claim. $ω(360) = 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 quantities such as the distinct-prime-count function. In this setting $ω(n)$ simply tallies the distinct primes dividing $n$, without reference to multiplicity or Dirichlet inversion. The surrounding file keeps statements minimal so that deeper algebraic identities can be added once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the definition of omega at 360 directly.
why it matters
This supplies a concrete numerical anchor inside the arithmetic-functions library that can support later prime-factor or Möbius calculations in the NumberTheory.Primes hierarchy. No downstream uses are recorded, so the result functions as a verified constant rather than a lemma feeding a larger chain. It remains peripheral to the Recognition Science forcing steps T0-T8 and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.