omega_twothousandthreehundredten
plain-language theorem explainer
The declaration asserts that the number of distinct prime factors of 2310 equals five. Number theorists checking small factorization tables or arithmetic function values would cite this when confirming explicit cases. The proof reduces to a single native evaluation step that computes the function directly on the integer.
Claim. $ω(2310) = 5$, where $ω(n)$ denotes the number of distinct prime factors of the positive integer $n$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. This declaration concerns the omega function, which counts distinct prime factors and sits alongside the bigOmega function that counts prime factors with multiplicity. The local setting keeps statements minimal to allow later layering of Dirichlet algebra and inversion formulas.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the omega function on 2310.
why it matters
This supplies a verified concrete value for the omega function on the integer whose prime factors are the first five primes. It supports the arithmetic functions infrastructure inside the NumberTheory.Primes module. No direct connection to the Recognition Science forcing chain, J-uniqueness, or phi-ladder is present, yet such base cases can anchor larger number-theoretic arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.