mathlib

fc790892 - feat(number_theory/primorial): Bound on the primorial function (#2701)

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.