vonMangoldt
plain-language theorem explainer
The von Mangoldt function is supplied as a direct alias to the standard arithmetic function that returns log p on prime powers p^k and zero elsewhere. Number theorists building the prime number theorem port would cite this wrapper when constructing the Chebyshev psi sum or the weak PNT hypothesis. The implementation is a one-line alias to Mathlib's ArithmeticFunction.vonMangoldt.
Claim. The von Mangoldt arithmetic function is the map from natural numbers to reals that satisfies Lambda(n) = log p whenever n equals p^k for prime p and integer k at least 1, and Lambda(n) = 0 otherwise.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Moebius function and extending to the von Mangoldt function. Arithmetic functions here are maps from naturals to reals used for encoding multiplicative structure in Dirichlet series and sums over divisors. The local setting keeps statements minimal until deeper inversion formulas stabilize.
proof idea
The declaration is a one-line wrapper that aliases Mathlib's ArithmeticFunction.vonMangoldt.
why it matters
This definition supplies the von Mangoldt function to the Chebyshev psi construction and the weak prime number theorem scaffold in the PNT port. It fills the arithmetic function interface needed for sums that appear in the prime number theorem derivations. The module positions these as footholds for Dirichlet algebra once the basic interfaces stabilize.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.