Primorial #

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.

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

theorem primorial_succ {n : ℕ} (hn1 : n ≠ 1) (hn : odd n) :

theorem primorial_add (m n : ℕ) :

theorem primorial_add_dvd {m n : ℕ} (h : n ≤ m) :

theorem primorial_add_le {m n : ℕ} (h : n ≤ m) :

theorem primorial_le_4_pow (n : ℕ) :