Primorial #
This file defines the primorial function (the product of primes less than or equal to some bound),
and proves that primorial n ≤ 4 ^ n
.
Notations #
We use the local notation n#
for the primorial of n
: that is, the product of the primes less
than or equal to n
.
theorem
primorial_add
(m : ℕ)
(n : ℕ)
:
primorial (m + n) = primorial m * Finset.prod (Finset.filter Nat.Prime (Finset.Ico (m + 1) (m + n + 1))) fun p => p