# mathlibdocumentation

number_theory.primorial

# 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.

def primorial  :

The primorial n# of n is the product of the primes less than or equal to n.

Equations
theorem primorial_succ {n : } :
1 < nn % 2 = 1primorial (n + 1) =

theorem dvd_choose_of_middling_prime (p : ) (is_prime : nat.prime p) (m : ) :
m + 1 < pp 2 * m + 1p (2 * m + 1).choose (m + 1)

theorem prod_primes_dvd {s : finset } (n : ) :
(∀ (a : ), a s(∀ (a : ), a sa n)∏ (p : ) in s, p n

theorem primorial_le_4_pow (n : ) :
4 ^ n