primeCounting'_eq_zero_iff

Mathlib.NumberTheory.PrimeCounting

URI: https://scilib.ai/kg/mathlib#Nat.primeCounting'_eq_zero_iff

← MathLib Explorer

English

π'(n) = 0 if and only if n ≤ 2.

Русский

π'(n) равно нулю тогда и только тогда, когда n ≤ 2.

LaTeX

$$$\pi'(n) = 0 \iff n \le 2$$$

Lean4

@[simp]
theorem primeCounting'_eq_zero_iff {n : ℕ} : n.primeCounting' = 0 ↔ n ≤ 2 := by
  rw [primeCounting', Nat.count_eq_zero ⟨_, Nat.prime_two⟩, Nat.nth_prime_zero_eq_two]

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

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

Разделы

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

Аффилиация

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