vonMangoldt_apply

Mathlib.NumberTheory.VonMangoldt

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

English

For any n, Λ(n) equals log(minFac(n)) if n is a prime power; otherwise Λ(n) = 0.

Русский

Для любого n: Λ(n) равно log(minFac(n)) если n является степенью простого; иначе Λ(n) = 0.

LaTeX

$$$$\Lambda(n) = \begin{cases} \log(\min Fac(n)), & \text{IsPrimePow}(n), \\ 0, & \text{otherwise}. \end{cases}$$$$

Lean4

theorem vonMangoldt_apply {n : ℕ} : Λ n = if IsPrimePow n then Real.log (minFac n) else 0 :=
  rfl

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

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

Разделы

Аффилиация

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