vonMangoldt_eq_zero_iff

Mathlib.NumberTheory.VonMangoldt

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

English

Λ(n) = 0 iff ¬IsPrimePow(n).

Русский

Λ(n) = 0 эквивалентно не является степенью простого.

LaTeX

$$$$\Lambda(n) = 0 \iff \neg IsPrimePow(n).$$$$

Lean4

theorem vonMangoldt_eq_zero_iff {n : ℕ} : Λ n = 0 ↔ ¬IsPrimePow n :=
  vonMangoldt_ne_zero_iff.not_right

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

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

Разделы

Аффилиация

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