mobius_ten
plain-language theorem explainer
The declaration establishes that the Möbius function evaluates to 1 at 10. Number theorists applying Möbius inversion to small integers or verifying convolution identities would reference this value. The proof is a direct native computation of the arithmetic function at that point.
Claim. $μ(10) = 1$, where $μ$ is the Möbius function from natural numbers to integers.
background
The Möbius function is supplied as an arithmetic function ℕ → ℤ via a direct wrapper around Mathlib's implementation. This module supplies lightweight statements for the function to enable later Dirichlet algebra and inversion formulas. The upstream definition states: The Möbius function (as an arithmetic function ℕ → ℤ).
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the arithmetic function directly at 10.
why it matters
This evaluation provides a concrete foothold inside the arithmetic functions module for building Möbius inversion tools. It fills a basic verification step in the NumberTheory.Primes hierarchy before deeper convolution identities are layered on. No downstream theorems depend on it yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.