primeCounting' — Mathlib

English

A variant of the prime counting function that counts primes strictly less than the input. Denoted by π'.

Русский

Вариант функции счёта простых чисел, считающий простые строго меньше данного аргумента. Обозначается π'.

LaTeX

$$$$ \\pi'(n) = \\#\\{ p:\\, p\\ \\text{prime} \\mid p < n \\} $$$$

Lean4

/-- A variant of the traditional prime counting function which gives the number of primes
*strictly* less than the input. More convenient for avoiding off-by-one errors.

With `open scoped Nat.Prime`, this has notation `π'`. -/
def primeCounting' : ℕ → ℕ :=
  Nat.count Prime

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