moebius_mul_log_eq_vonMangoldt

Mathlib.NumberTheory.VonMangoldt

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

English

The Möbius convolution with the logarithm also yields von Mangoldt: μ * log = Λ.

Русский

С Möbius-свёрткой логарифма тоже получается Λ: μ * log = Λ.

LaTeX

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

Lean4

@[simp]
theorem moebius_mul_log_eq_vonMangoldt : (μ : ArithmeticFunction ℝ) * log = Λ := by rw [mul_comm]; simp

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

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

Разделы

Аффилиация

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