THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file defines the primorial function (the product of primes less than or equal to some bound),
and proves that
primorial n ≤ 4 ^ n.
We use the local notation
n# for the primorial of
n: that is, the product of the primes less
than or equal to
n is the product of the primes less than or equal to