mobius_twelve
plain-language theorem explainer
The declaration establishes that the Möbius function evaluates to zero at 12. Number theorists applying Möbius inversion or checking squarefreeness would reference this concrete case when handling composite arguments divisible by squares. The proof is a one-line wrapper that invokes native_decide to compute the arithmetic function value directly.
Claim. $μ(12) = 0$, where $μ$ denotes the Möbius function as an arithmetic function from natural numbers to integers.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. The upstream definition states: 'The Möbius function (as an arithmetic function ℕ → ℤ)'. This abbrev maps to ArithmeticFunction.moebius and supports basic squarefreeness checks in the NumberTheory.Primes context. The module keeps statements lightweight, with deeper Dirichlet algebra and inversion to be layered on once basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the Möbius function at 12 and confirm equality to zero.
why it matters
This supplies a concrete evaluation of the Möbius function for a non-squarefree argument, supporting arithmetic function development in the NumberTheory.Primes module. No downstream theorems are recorded yet. It aligns with the module's role in providing footholds for later inversion results without addressing general formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.