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.

Notation

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.

@[simp]

theorem primorial_zero : primorial 0 = 1

@[simp]

theorem primorial_one : primorial 1 = 1

@[simp]

theorem primorial_two : primorial 2 = 2

theorem primorial_pos (n : ℕ) : 0 < primorial n

theorem primorial_mono {m n : ℕ} (h : m ≤ n) : primorial m ≤ primorial n

theorem primorial_monotone : Monotone primorial

theorem primorial_dvd_primorial {m n : ℕ} (h : m ≤ n) : primorial m ∣ primorial n

theorem primorial_succ {n : ℕ} (hn1 : n ≠ 1) (hn : Odd n) : primorial (n + 1) = primorial n

theorem primorial_add (m n : ℕ) : primorial (m + n) = primorial m * ∏ p ∈ Finset.Ico (m + 1) (m + n + 1) with Nat.Prime p, p

theorem primorial_add_dvd {m n : ℕ} (h : n ≤ m) : primorial (m + n) ∣ primorial m * (m + n).choose m

theorem primorial_add_le {m n : ℕ} (h : n ≤ m) : primorial (m + n) ≤ primorial m * (m + n).choose m

theorem Nat.Prime.dvd_primorial_iff {p n : ℕ} (hp : Prime p) : p ∣ primorial n ↔ p ≤ n

theorem Nat.Prime.dvd_primorial {p : ℕ} (hp : Prime p) : p ∣ primorial p

theorem Squarefree.dvd_primorial {n : ℕ} (hn : Squarefree n) : n ∣ primorial n

theorem lt_primorial_self {n : ℕ} (hn : 2 < n) : n < primorial n

theorem le_primorial_self {n : ℕ} : n ≤ primorial n

theorem primorial_lt_four_pow (n : ℕ) (hn : n ≠ 0) : primorial n < 4 ^ n

theorem primorial_le_four_pow (n : ℕ) : primorial n ≤ 4 ^ n

@[deprecated primorial_le_four_pow (since := "2026-03-21")]

theorem primorial_le_4_pow (n : ℕ) : primorial n ≤ 4 ^ n

Alias of primorial_le_four_pow.