omega_twohundredten
plain-language theorem explainer
The declaration asserts that the arithmetic function counting distinct prime factors evaluates to exactly 4 at 210. Number theorists using Möbius inversion or squarefree checks for this integer would reference the value as a verified constant. The proof proceeds by direct evaluation via native_decide without explicit factorization steps.
Claim. $ω(210) = 4$, where $ω(n)$ denotes the number of distinct prime factors of the positive integer $n$.
background
This theorem belongs to the module supplying lightweight wrappers around Mathlib's arithmetic function library, with initial focus on the Möbius function μ. The omega function (implemented as bigOmega) returns the count of distinct primes dividing its argument. The module maintains minimal statements to enable later layering of Dirichlet algebra and inversion once core interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate omega 210 by direct computation.
why it matters
The result supplies a concrete base evaluation inside the arithmetic functions module for the squarefree integer 210 = 2·3·5·7. It supports the Möbius footholds section without feeding any downstream theorems at present. No direct link to Recognition Science forcing chain steps or constants appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.