vonMangoldt_ne_zero_iff

Mathlib.NumberTheory.VonMangoldt

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$$\Lambda(n) \neq 0 \iff \text{IsPrimePow}(n).$$$$

Lean4

theorem vonMangoldt_ne_zero_iff {n : ℕ} : Λ n ≠ 0 ↔ IsPrimePow n :=
  by
  rcases eq_or_ne n 1 with (rfl | hn); · simp [not_isPrimePow_one]
  exact (Real.log_pos (one_lt_cast.2 (minFac_prime hn).one_lt)).ne'.ite_ne_right_iff

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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