Theorem Nat.primesBelow_card_eq_primeCounting'

Modification history

2026-05-11 16:00

Mathlib/NumberTheory/PrimeCounting.lean

feat: lower bounds for Chebyshev theta and psi functions (#38986) …

Modified Nat.primesBelow_card_eq_primeCounting'View on Github →

2024-10-23 02:43

Mathlib/NumberTheory/PrimeCounting.lean

chore: use newly introduced finset notation (#17974) …

Modified Nat.primesBelow_card_eq_primeCounting'View on Github →

2024-09-24 06:31

Mathlib/NumberTheory/PrimeCounting.lean

feat(NumberTheory/PrimeCounting): surjective and tendsto (#17006)

Modified Nat.primesBelow_card_eq_primeCounting'View on Github →

2023-11-11 15:52

Mathlib/NumberTheory/PrimeCounting.lean

feat: add definition of and statements about the set of smooth numbers (#8252) …

Added Nat.primesBelow_card_eq_primeCounting'View on Github →