Documentation

Mathlib.NumberTheory.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
Instances For
    theorem primorial_pos (n : ) :
    theorem primorial_succ {n : } (hn1 : n 1) (hn : Odd n) :
    theorem primorial_add (m : ) (n : ) :
    primorial (m + n) = primorial m * Finset.prod (Finset.filter Nat.Prime (Finset.Ico (m + 1) (m + n + 1))) fun (p : ) => p
    theorem primorial_add_dvd {m : } {n : } (h : n m) :
    theorem primorial_add_le {m : } {n : } (h : n m) :