vonMangoldt_eq_zero_of_not_prime_pow
plain-language theorem explainer
The von Mangoldt function vanishes on every natural number that fails to be a prime power. Analysts working with Dirichlet series or prime-power sums would cite the vanishing rule to truncate convolutions. The argument is a one-line simplification that unfolds the definition and applies the standard characterization from Mathlib.
Claim. Let $n$ be a natural number. If $n$ is not a prime power, then the von Mangoldt function satisfies $Λ(n)=0$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to the von Mangoldt function. The von Mangoldt function is introduced as the standard map that records log p on prime powers p^k and is defined via the abbreviation vonMangoldt for ArithmeticFunction.vonMangoldt. The local setting keeps statements minimal so that deeper Dirichlet algebra can be added once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that unfolds vonMangoldt and applies the right-to-left direction of ArithmeticFunction.vonMangoldt_eq_zero_iff to the hypothesis that n is not a prime power.
why it matters
The declaration supplies the basic vanishing property for Λ that supports prime-power restrictions in arithmetic-function calculations inside the NumberTheory.Primes layer. It fills the explicit statement given in the module doc-comment and aligns with the framework's use of standard number-theoretic tools ahead of any forcing-chain applications. No downstream uses appear in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.