Commit 2023-06-21 11:07 c9f26d2c

View on Github →

feat: port NumberTheory.PrimeCounting (#5342)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/PrimeCounting.lean

added theorem Nat.monotone_primeCounting'

added theorem Nat.monotone_primeCounting

added def Nat.primeCounting'

added theorem Nat.primeCounting'_add_le

added theorem Nat.primeCounting'_nth_eq

added def Nat.primeCounting

added theorem Nat.prime_nth_prime