Metamath Proof Explorer


Table of Contents - 6.1.11. The least common multiple

According to Wikipedia ("Least common multiple", 27-Aug-2020, https://en.wikipedia.org/wiki/Least_common_multiple): "In arithmetic and number theory, the least common multiple, lowest common multiple, or smallest common multiple of two integers a and b, usually denoted by lcm(a, b), is the smallest positive integer that is divisible by both a and b. Since division of integers by zero is undefined, this definition has meaning only if a and b are both different from zero. However, some authors define lcm(a,0) as 0 for all a, which is the result of taking the lcm to be the least upper bound in the lattice of divisibility. ... The lcm of more than two integers is also well-defined: it is the smallest positive integer hat is divisible by each of them."

In this section, an operation calculating the least common multiple of two integers (df-lcm) as well as a function mapping a set of integers to their least common multiple (df-lcmf) are provided. Both definitions are valid for all integers, including negative integers and 0, obeying the above mentioned convention. It is shown by lcmfpr that the two definitions are compatible.

  1. clcm
  2. clcmf
  3. df-lcm
  4. df-lcmf
  5. lcmval
  6. lcmcom
  7. lcm0val
  8. lcmn0val
  9. lcmcllem
  10. lcmn0cl
  11. dvdslcm
  12. lcmledvds
  13. lcmeq0
  14. lcmcl
  15. gcddvdslcm
  16. lcmneg
  17. neglcm
  18. lcmabs
  19. lcmgcdlem
  20. lcmgcd
  21. lcmdvds
  22. lcmid
  23. lcm1
  24. lcmgcdnn
  25. lcmgcdeq
  26. lcmdvdsb
  27. lcmass
  28. 3lcm2e6woprm
  29. 6lcm4e12
  30. absproddvds
  31. absprodnn
  32. fissn0dvds
  33. fissn0dvdsn0
  34. lcmfval
  35. lcmf0val
  36. lcmfn0val
  37. lcmfnnval
  38. lcmfcllem
  39. lcmfn0cl
  40. lcmfpr
  41. lcmfcl
  42. lcmfnncl
  43. lcmfeq0b
  44. dvdslcmf
  45. lcmfledvds
  46. lcmf
  47. lcmf0
  48. lcmfsn
  49. lcmftp
  50. lcmfunsnlem1
  51. lcmfunsnlem2lem1
  52. lcmfunsnlem2lem2
  53. lcmfunsnlem2
  54. lcmfunsnlem
  55. lcmfdvds
  56. lcmfdvdsb
  57. lcmfunsn
  58. lcmfun
  59. lcmfass
  60. lcmf2a3a4e12
  61. lcmflefac