Commit 2022-03-11 06:44 3061d18f

View on Github →

feat(data/nat/{nth,prime}): add facts about primes (#12560) Gives {p | prime p}.infinite as well as infinite_of_not_bdd_above lemma. Also gives simp lemmas for prime_counting'.

Estimated changes

Modified src/data/nat/nth.lean

added theorem nat.nth_injective_of_infinite

Modified src/data/nat/prime.lean

added theorem nat.infinite_set_of_prime

added theorem nat.not_bdd_above_set_of_prime

Modified src/data/set/finite.lean

added theorem set.infinite_of_not_bdd_above

added theorem set.infinite_of_not_bdd_below

Modified src/number_theory/prime_counting.lean

added theorem nat.prime_counting'_nth_eq

added theorem nat.prime_nth_prime