vonMangoldt_pos_iff

Mathlib.NumberTheory.VonMangoldt

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

English

0 < Λ(n) iff IsPrimePow(n).

Русский

0 < Λ(n) тогда и только тогда, когда n — простая степень.

LaTeX

$$$$0 < \Lambda(n) \iff IsPrimePow(n).$$$$

Lean4

theorem vonMangoldt_pos_iff {n : ℕ} : 0 < Λ n ↔ IsPrimePow n :=
  vonMangoldt_nonneg.lt_iff_ne.trans (ne_comm.trans vonMangoldt_ne_zero_iff)

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

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

Разделы

Аффилиация

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