On Square-Free Numbers

Adam Grabowski

Formalized Mathematics (2013)

  • Volume: 21, Issue: 2, page 153-162
  • ISSN: 1426-2630

Abstract

top
In the article the formal characterization of square-free numbers is shown; in this manner the paper is the continuation of [19]. Essentially, we prepared some lemmas for convenient work with numbers (including the proof that the sequence of prime reciprocals diverges [1]) according to [18] which were absent in the Mizar Mathematical Library. Some of them were expressed in terms of clusters’ registrations, enabling automatization machinery available in the Mizar system. Our main result of the article is in the final section; we proved that the lattice of positive divisors of a positive integer n is Boolean if and only if n is square-free.

How to cite

top

Adam Grabowski. "On Square-Free Numbers." Formalized Mathematics 21.2 (2013): 153-162. <http://eudml.org/doc/266799>.

@article{AdamGrabowski2013,
abstract = {In the article the formal characterization of square-free numbers is shown; in this manner the paper is the continuation of [19]. Essentially, we prepared some lemmas for convenient work with numbers (including the proof that the sequence of prime reciprocals diverges [1]) according to [18] which were absent in the Mizar Mathematical Library. Some of them were expressed in terms of clusters’ registrations, enabling automatization machinery available in the Mizar system. Our main result of the article is in the final section; we proved that the lattice of positive divisors of a positive integer n is Boolean if and only if n is square-free.},
author = {Adam Grabowski},
journal = {Formalized Mathematics},
keywords = {square-free numbers; prime reciprocals; lattice of natural divisors},
language = {eng},
number = {2},
pages = {153-162},
title = {On Square-Free Numbers},
url = {http://eudml.org/doc/266799},
volume = {21},
year = {2013},
}

TY - JOUR
AU - Adam Grabowski
TI - On Square-Free Numbers
JO - Formalized Mathematics
PY - 2013
VL - 21
IS - 2
SP - 153
EP - 162
AB - In the article the formal characterization of square-free numbers is shown; in this manner the paper is the continuation of [19]. Essentially, we prepared some lemmas for convenient work with numbers (including the proof that the sequence of prime reciprocals diverges [1]) according to [18] which were absent in the Mizar Mathematical Library. Some of them were expressed in terms of clusters’ registrations, enabling automatization machinery available in the Mizar system. Our main result of the article is in the final section; we proved that the lattice of positive divisors of a positive integer n is Boolean if and only if n is square-free.
LA - eng
KW - square-free numbers; prime reciprocals; lattice of natural divisors
UR - http://eudml.org/doc/266799
ER -

References

top
  1. [1] M. Aigner and G. M. Ziegler. Proofs from THE BOOK. Springer-Verlag, Berlin Heidelberg New York, 2004. Zbl1098.00001
  2. [2] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990. 
  3. [3] Grzegorz Bancerek. K¨onig’s theorem. Formalized Mathematics, 1(3):589-593, 1990. 
  4. [4] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. Zbl06213858
  5. [5] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990. 
  6. [6] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990. 
  7. [7] Józef Białas. Group and field definitions. Formalized Mathematics, 1(3):433-439, 1990. 
  8. [8] Czesław Bylinski. Binary operations. Formalized Mathematics, 1(1):175-180, 1990. 
  9. [9] Czesław Bylinski. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529-536, 1990. 
  10. [10] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990. 
  11. [11] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  12. [12] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990. 
  13. [13] Czesław Bylinski. The sum and product of finite sequences of real numbers. Formalized Mathematics, 1(4):661-668, 1990. 
  14. [14] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  15. [15] Marek Chmur. The lattice of natural numbers and the sublattice of it. The set of prime numbers. Formalized Mathematics, 2(4):453-459, 1991. 
  16. [16] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990. 
  17. [17] Yoshinori Fujisawa, Yasushi Fuwa, and Hidetaka Shimizu. Public-key cryptography and Pepin’s test for the primality of Fermat numbers. Formalized Mathematics, 7(2):317-321, 1998. 
  18. [18] G.H. Hardy and E.M. Wright. An Introduction to the Theory of Numbers. Oxford University Press, 1980. Zbl0020.29201
  19. [19] Magdalena Jastrz¸ebska and Adam Grabowski. On the properties of the M¨obius function. Formalized Mathematics, 14(1):29-36, 2006. doi:10.2478/v10037-006-0005-0.[Crossref] 
  20. [20] Andrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5): 841-845, 1990. 
  21. [21] Andrzej Kondracki. The Chinese Remainder Theorem. Formalized Mathematics, 6(4): 573-577, 1997. 
  22. [22] Artur Korniłowicz. On the real valued functions. Formalized Mathematics, 13(1):181-187, 2005. 
  23. [23] Artur Korniłowicz and Piotr Rudnicki. Fundamental Theorem of Arithmetic. Formalized Mathematics, 12(2):179-186, 2004. 
  24. [24] Jarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269-272, 1990. 
  25. [25] Jarosław Kotowicz. Convergent sequences and the limit of sequences. Formalized Mathematics, 1(2):273-275, 1990. 
  26. [26] Rafał Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887-890, 1990. 
  27. [27] Rafał Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relatively primes. Formalized Mathematics, 1(5):829-832, 1990. 
  28. [28] Xiquan Liang, Li Yan, and Junjie Zhao. Linear congruence relation and complete residue systems. Formalized Mathematics, 15(4):181-187, 2007. doi:10.2478/v10037-007-0022-7.[Crossref] 
  29. [29] Robert Milewski. Natural numbers. Formalized Mathematics, 7(1):19-22, 1998. 
  30. [30] Adam Naumowicz. Conjugate sequences, bounded complex sequences and convergent complex sequences. Formalized Mathematics, 6(2):265-268, 1997. 
  31. [31] Hiroyuki Okazaki and Yasunari Shidama. Uniqueness of factoring an integer and multiplicative group Z/pZ*. Formalized Mathematics, 16(2):103-107, 2008. doi:10.2478/v10037-008-0015-1.[Crossref] 
  32. [32] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147-152, 1990. 
  33. [33] Konrad Raczkowski and Andrzej Nedzusiak. Series. Formalized Mathematics, 2(4):449-452, 1991. 
  34. [34] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25-34, 1990. 
  35. [35] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1 (2):329-334, 1990. 
  36. [36] Andrzej Trybulec. On the sets inhabited by numbers. Formalized Mathematics, 11(4): 341-347, 2003. 
  37. [37] Andrzej Trybulec. Many sorted sets. Formalized Mathematics, 4(1):15-22, 1993. 
  38. [38] Andrzej Trybulec and Czesław Bylinski. Some properties of real numbers. Formalized Mathematics, 1(3):445-449, 1990. 
  39. [39] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990. 
  40. [40] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  41. [41] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990. 
  42. [42] Stanisław Zukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215-222, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.