Commit 2020-05-26 13:30 fc790892

View on Github →

feat(number_theory/primorial): Bound on the primorial function (#2701) This lemma is needed for Erdös's proof of Bertrand's postulate, but it may be of independent interest.

Estimated changes

Modified src/data/finset.lean

added theorem finset.self_mem_range_succ

Modified src/data/list/range.lean

added theorem list.self_mem_range_succ

Modified src/data/multiset.lean

added theorem multiset.self_mem_range_succ

Modified src/data/nat/basic.lean

added theorem nat.choose_symm_half

Modified src/data/nat/choose.lean

modified theorem choose_le_middle

added theorem choose_middle_le_pow

Created src/number_theory/primorial.lean

added theorem dvd_choose_of_middling_prime

added def primorial

added theorem primorial_le_4_pow

added theorem primorial_succ

added theorem prod_primes_dvd