mobius_twothousandthreehundredten
plain-language theorem explainer
The Möbius function evaluates to -1 at 2310, confirming the integer is square-free with five distinct prime factors. Analytic number theorists working on Dirichlet inversion or inclusion-exclusion would reference this explicit value for calculations involving 2310. The proof is a direct computational check via native_decide on the arithmetic-function definition.
Claim. $μ(2310) = -1$, where $μ$ is the Möbius arithmetic function from $ℕ$ to $ℤ$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function $μ$ (implemented as the abbrev mobius for ArithmeticFunction.moebius). By definition $μ(n)$ returns 0 when $n$ is not square-free and otherwise equals $(-1)^k$ for $k$ the number of distinct prime factors. The local setting is a collection of small footholds for later Dirichlet algebra and inversion, kept deliberately lightweight.
proof idea
One-line wrapper that applies native_decide to evaluate the Möbius function at 2310.
why it matters
This supplies a concrete numerical instance inside the arithmetic-functions module, verifying the expected sign for a product of five distinct primes. No downstream theorems currently cite it, but it supports explicit checks that can feed into broader prime-factorization or square-free properties. It stays within the module's stated scope of basic interfaces rather than touching Recognition Science forcing chains or constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.