# 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 (n : ) :

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

Equations
theorem primorial_succ {n : } (n_big : 1 < n) (r : n % 2 = 1) :
primorial (n + 1) =
theorem dvd_choose_of_middling_prime (p : ) (is_prime : nat.prime p) (m : ) (p_big : m + 1 < p) (p_small : p 2 * m + 1) :
p (2 * m + 1).choose (m + 1)
theorem primorial_le_4_pow (n : ) :
4 ^ n