Metamath Proof Explorer

Table of Contents - 6.2.15. Primorial function

According to Wikipedia "Primorial", (28-Aug-2020): "In mathematics, and more particularly in number theory, primorial, denoted by "#", is a function from natural numbers to natural numbers similar to the factorial function, but rather than successively multiplying [all] positive integers [less than or equal to a given number], the function only multiplies [the] prime numbers [less than or equal to the given number]. The name "primorial", coined by Harvey Dubner, draws an analogy to primes similar to the way the name "factorial" relates to factors."

  1. cprmo
  2. df-prmo
  3. prmoval
  4. prmocl
  5. prmone0
  6. prmo0
  7. prmo1
  8. prmop1
  9. prmonn2
  10. prmo2
  11. prmo3
  12. prmdvdsprmo
  13. prmdvdsprmop
  14. fvprmselelfz
  15. fvprmselgcd1
  16. prmolefac
  17. prmodvdslcmf
  18. prmolelcmf