primeCounting'_nth_eq — Mathlib

English

Let p_n denote the nth prime. Then the prime-counting function evaluated at p_n equals n, i.e., π'(p_n) = n.

Русский

Пусть p_n обозначает n-е простое число. Тогда значение функции подсчета простых чисел до p_n равно n, т.е. π'(p_n) = n.

LaTeX

$$$\pi'(p_n) = n$$$

Lean4

@[simp]
theorem primeCounting'_nth_eq (n : ℕ) : π' (nth Prime n) = n :=
  count_nth_of_infinite infinite_setOf_prime _

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