mobius_one
plain-language theorem explainer
μ(1) equals 1 by the standard definition of the Möbius function. Number theorists applying Möbius inversion or Dirichlet convolution reference this evaluation as the base case. The proof reduces immediately to the underlying arithmetic function via simplification.
Claim. The Möbius function satisfies $μ(1) = 1$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function μ as an arithmetic function from natural numbers to integers. The upstream abbrev defines mobius directly as ArithmeticFunction.moebius, providing the core object for all statements in this file. The local setting keeps statements minimal to allow later layering of Dirichlet algebra and inversion once interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies the definition of mobius via simplification.
why it matters
This evaluation anchors the Möbius function properties inside the arithmetic functions module. It supplies the base case needed for any subsequent inversion or convolution work, even though the current dependency graph lists no direct dependents. The result fills the initial foothold described in the module documentation before deeper number-theoretic tools are added.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.