moebius_mul_zeta
plain-language theorem explainer
The theorem establishes that the Möbius arithmetic function multiplied by the constant-one zeta function equals the Dirichlet unit function. Number theorists cite this as the starting point for all Möbius inversion formulas. The proof is a one-line wrapper that unfolds the local abbreviations and invokes Mathlib's built-in identity.
Claim. $μ * ζ = ε$, where $μ$ is the Möbius arithmetic function, $ζ$ is the constant function 1 on positive integers, and $ε$ is the unit function (1 at 1, 0 elsewhere) under Dirichlet convolution.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The Möbius function is the arithmetic function ℕ → ℤ given by the standard definition (sum of (-1)^k over square-free divisors). Zeta is the arithmetic zeta function, the constant function 1 on positive integers. The local setting is described as: 'This file provides small wrappers around Mathlib's arithmetic function library, starting with the Möbius function μ (spelled ArithmeticFunction.moebius in code). We keep the statements lightweight here; deeper Dirichlet algebra and inversion can be layered on once the basic interfaces stabilize.'
proof idea
The proof is a one-line wrapper. It first unfolds the abbreviations mobius and zeta via simp, then applies the Mathlib theorem ArithmeticFunction.moebius_mul_coe_zeta directly.
why it matters
This supplies the identity μ * ζ = ε that the module documentation calls 'the foundation of Möbius inversion.' It is the arithmetic counterpart of the fact that the sum of μ(d) over d dividing n equals 1 if n=1 and 0 otherwise. In the Recognition Science monolith it provides the inversion tool required for later prime-counting and divisor-sum arguments, even though no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.