Commit 2022-01-29 20:28 4085363d

View on Github →

feat(number_theory/prime_counting): The prime counting function (#9080) With an eye to implementing this proof, I am adding a file to define the prime counting function and prove a simple upper bound on it.

Estimated changes

Modified src/data/nat/totient.lean

added theorem nat.Ico_filter_coprime_le

added theorem nat.filter_coprime_Ico_eq_totient

modified def nat.totient

modified theorem nat.totient_eq_card_coprime

Created src/number_theory/prime_counting.lean

added theorem nat.monotone_prime_counting'

added theorem nat.monotone_prime_counting

added def nat.prime_counting'

added theorem nat.prime_counting'_add_le

added def nat.prime_counting

Modified src/set_theory/fincard.lean

deleted def nat.card

modified theorem nat.card_eq_fintype_card

modified theorem nat.card_eq_zero_of_infinite