# mathlib3documentation

number_theory.von_mangoldt

# The von Mangoldt Function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define the von Mangoldt function: the function on natural numbers that returns log p if the input can be expressed as p^k for a prime p.

## Main Results #

The main definition for this file is

• nat.arithmetic_function.von_mangoldt: The von Mangoldt function Λ.

We then prove the classical summation property of the von Mangoldt function in nat.arithmetic_function.von_mangoldt_sum, that ∑ i in n.divisors, Λ i = real.log n, and use this to deduce alternative expressions for the von Mangoldt function via Möbius inversion, see nat.arithmetic_function.sum_moebius_mul_log_eq.

## Notation #

We use the standard notation Λ to represent the von Mangoldt function.

noncomputable def nat.arithmetic_function.log  :

log as an arithmetic function ℕ → ℝ. Note this is in the nat.arithmetic_function namespace to indicate that it is bundled as an arithmetic_function rather than being the usual real logarithm.

Equations
@[simp]
noncomputable def nat.arithmetic_function.von_mangoldt  :

The von_mangoldt function is the function on natural numbers that returns log p if the input can be expressed as p^k for a prime p. In the case when n is a prime power, min_fac will give the appropriate prime, as it is the smallest prime factor.

In the arithmetic_function locale, we have the notation Λ for this function.

Equations
@[simp]
@[simp]