log_mul_moebius_eq_vonMangoldt

Mathlib.NumberTheory.VonMangoldt

URI: https://scilib.ai/kg/mathlib#ArithmeticFunction.log_mul_moebius_eq_vonMangoldt

English

Convolution of the logarithm with Möbius equals von Mangoldt: log * μ = Λ.

Русский

Свёртка логарифма с Möbius даёт Λ: log * μ = Λ.

LaTeX

$$$$ (\log * \mu)(n) = \Lambda(n). $$$$

Lean4

@[simp]
theorem log_mul_moebius_eq_vonMangoldt : log * μ = Λ := by
  rw [← vonMangoldt_mul_zeta, mul_assoc, coe_zeta_mul_coe_moebius, mul_one]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru