mobius_twenty
plain-language theorem explainer
The Möbius function vanishes at 20 because 20 is divisible by 4. Number theorists applying inclusion-exclusion or Dirichlet inversion cite this evaluation as a routine check. The proof is a one-line native_decide that computes the value directly from the arithmetic definition.
Claim. $μ(20) = 0$, where $μ$ is the Möbius function.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function $μ$ (aliased as an ArithmeticFunction ℕ → ℤ). The local setting keeps statements minimal so that Dirichlet convolution and inversion can be added once interfaces stabilize. The upstream mobius abbrev directly aliases ArithmeticFunction.moebius, providing the concrete map used in the claim.
proof idea
One-line wrapper that applies native_decide to evaluate the arithmetic function at the concrete input 20.
why it matters
The result supplies a basic squarefree check inside the Möbius footholds of the NumberTheory layer. It supports later arithmetic identities required by the Recognition framework, even though no downstream uses are recorded yet. The placement after the general mobius definition and before further squarefree examples indicates it closes a small verification gap in the arithmetic-function scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.