mathlib

4085363d - feat(number_theory/prime_counting): The prime counting function (#9080)

feat(number_theory/prime_counting): The prime counting function (#9080) With an eye to implementing [this proof](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238002/near/251178921), I am adding a file to define the prime counting function and prove a simple upper bound on it. Co-authored-by: Vladimir Goryachev <gor050299@gmail.com> Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: YaelDillies <yael.dillies@gmail.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Eric <ericrboidi@gmail.com>