mobius_fortytwo
plain-language theorem explainer
The declaration establishes that the Möbius function evaluates to negative one at 42. Number theorists checking arithmetic function signs for squarefree composites with three distinct prime factors would cite this instance. The proof is a one-line wrapper that applies native_decide to the definition of the Möbius function.
Claim. $μ(42) = -1$, where $μ$ is the Möbius function from natural numbers to integers.
background
The Möbius function $μ$ maps a natural number to an integer: it returns zero if the argument has a squared prime factor and otherwise equals $(-1)^k$ for $k$ the number of distinct prime factors. This module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function expressed as an ArithmeticFunction from naturals to integers. The upstream abbrev identifies mobius directly with the standard Möbius arithmetic function.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the arithmetic function at 42.
why it matters
This evaluation supplies a concrete check for the Möbius function inside the NumberTheory.Primes.ArithmeticFunctions module, which supplies footholds for later Dirichlet algebra and inversion steps. It confirms the sign expected for a squarefree integer with three prime factors, consistent with the general definition used throughout the prime arithmetic layer. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.