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) :

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 prod_primes_dvd {s : finset ℕ} (n : ℕ) (h : ∀ (a : ℕ), a ∈ s → nat.prime a) (div : ∀ (a : ℕ), a ∈ s → a ∣ n) :

∏ (p : ℕ) in s, p ∣ n

theorem primorial_le_4_pow (n : ℕ) :