vonMangoldt_prime_pow
plain-language theorem explainer
The theorem states that the von Mangoldt function evaluates to the natural log of p on any positive power of a prime p. Analytic number theorists working with Dirichlet series or prime-power sums would cite this identity to simplify explicit formulas. The proof converts the input hypotheses to native types, rewrites via the arithmetic-function definition, and reduces directly to the prime case lemma.
Claim. Let $p$ be a prime number and let $k$ be a positive integer. Then the von Mangoldt function satisfies $Λ(p^k) = log p$.
background
The von Mangoldt function is introduced in this module as the standard arithmetic function ℕ → ℝ that returns log p on prime powers p^k (k ≥ 1) and zero elsewhere; the module itself supplies lightweight wrappers around Mathlib's arithmetic-function library, beginning with the Möbius function and extending to related tools for Dirichlet algebra. The local setting is therefore one of basic number-theoretic interfaces that can later support inversion formulas once the core definitions stabilize. The proof depends on the abbrev vonMangoldt (which aliases ArithmeticFunction.vonMangoldt) together with the prior theorem vonMangoldt_prime that handles the k = 1 case.
proof idea
The term-mode proof first obtains Nat.Prime p from the supplied Prime hypothesis via the equivalence lemma, converts the positivity assumption on k into a nonzero statement, rewrites the target using the vonMangoldt definition and Mathlib's vonMangoldt_apply_pow rule, then finishes by exact application of the prime-case lemma vonMangoldt_prime.
why it matters
This identity supplies the exact evaluation of the von Mangoldt function on prime powers, which is required for any subsequent multiplicative or convolution identities in the arithmetic-functions layer. It sits inside the NumberTheory.Primes.ArithmeticFunctions module whose doc-comment frames the work as preparatory footholds for Dirichlet series; no immediate downstream theorems are recorded, yet the result closes the prime-power case needed for later extensions such as explicit formulas or Möbius inversion over prime powers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.