Theorems · Definition · number theory
primorial
ℕ → ℕ
The primorial n# of n is the product of the primes less than or equal to n.
- Defined in
- Mathlib.NumberTheory.Primorial
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 54 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finset.prodproof · cited by 2,356
- Nat.Primeproof · cited by 2,059
- Finset.rangeproof · cited by 1,341
- Finset.filterproof · cited by 949
Cited by26
Results whose statement or proof uses this declaration.
- Chebyshev.theta_le_log4_mul_xproof · cited by 4
- primorial_le_four_powstatement · cited by 3
- primorial_posstatement · cited by 3
- Nat.Prime.dvd_primorial_iffstatement and proof · cited by 2
- primorial_eq_prod_primesLEstatement · cited by 2
- lt_primorial_selfstatement and proof · cited by 1
- Chebyshev.theta_eq_log_primorialstatement · cited by 1
- primorial_addstatement · cited by 1
- primorial_add_dvdstatement and proof · cited by 1
- primorial_add_lestatement · cited by 1
- primorial_lt_four_powstatement and proof · cited by 1
- primorial_monostatement · cited by 1