mathlib3 documentation

number_theory.primorial

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 : ) :
primorial (m + n) = primorial m * (finset.filter nat.prime (finset.Ico (m + 1) (m + n + 1))).prod (λ (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 primorial_le_4_pow (n : ) :