mobius_onehundredfive
plain-language theorem explainer
The declaration establishes that the Möbius function evaluates to -1 at 105. Analytic number theorists performing explicit inclusion-exclusion or Dirichlet series calculations with the factorization 3·5·7 would cite this value. The proof is a one-line native decision that evaluates the arithmetic function definition directly.
Claim. $μ(105) = -1$, where $μ$ is the Möbius function on the positive integers.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function $μ$ defined as an arithmetic function from naturals to integers. The upstream definition identifies mobius with ArithmeticFunction.moebius, providing the standard map that returns (-1)^k on squarefree inputs with k prime factors and zero otherwise. This specific evaluation sits within the broader setup for Dirichlet algebra and inversion formulas once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the arithmetic function at 105 directly.
why it matters
This result supplies an explicit numerical foothold for the Möbius function inside the arithmetic functions module, supporting calculations that rely on the sign (-1)^k for squarefree numbers with an odd number of prime factors. It aligns with the module's role as a foundation for later inversion tools, though no downstream uses are recorded. It touches the open question of layering deeper Dirichlet algebra on these basic values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.