convolution_vonMangoldt_const_one

English

The Dirichlet convolution of the von Mangoldt function with the constant function 1 equals the complex logarithm function: (Λ * 1)(n) = log n.

Русский

Свёртка Λ с константой 1 равна логарифмической функции: (Λ * 1)(n) = log n.

LaTeX

$$$(\\Lambda * 1)(n) = \\log n$$$

Lean4

theorem convolution_vonMangoldt_const_one : ↗Λ ⍟ 1 = ↗Complex.log :=
  (convolution_one_eq_convolution_zeta _).trans convolution_vonMangoldt_zeta

Похожие утверждения