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.
@article{bwmeta1.element.doi-10_2478_forma-2013-0017,
author = {Adam Grabowski},
title = {On Square-Free Numbers},
journal = {Formalized Mathematics},
volume = {21},
year = {2013},
pages = {153-162},
zbl = {1298.11008},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_2478_forma-2013-0017}
}
Adam Grabowski. On Square-Free Numbers. Formalized Mathematics, Tome 21 (2013) pp. 153-162. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_2478_forma-2013-0017/
[1] M. Aigner and G. M. Ziegler. Proofs from THE BOOK. Springer-Verlag, Berlin Heidelberg New York, 2004. | Zbl 1098.00001
[2] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990.
[3] Grzegorz Bancerek. K¨onig’s theorem. Formalized Mathematics, 1(3):589-593, 1990.
[4] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. | Zbl 06213858
[5] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990.
[6] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990.
[7] Józef Białas. Group and field definitions. Formalized Mathematics, 1(3):433-439, 1990.
[8] Czesław Bylinski. Binary operations. Formalized Mathematics, 1(1):175-180, 1990.
[9] Czesław Bylinski. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529-536, 1990.
[10] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990.
[11] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.
[12] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990.
[13] Czesław Bylinski. The sum and product of finite sequences of real numbers. Formalized Mathematics, 1(4):661-668, 1990.
[14] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.
[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] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990.
[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] G.H. Hardy and E.M. Wright. An Introduction to the Theory of Numbers. Oxford University Press, 1980. | Zbl 0020.29201
[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] Andrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5): 841-845, 1990.
[21] Andrzej Kondracki. The Chinese Remainder Theorem. Formalized Mathematics, 6(4): 573-577, 1997.
[22] Artur Korniłowicz. On the real valued functions. Formalized Mathematics, 13(1):181-187, 2005.
[23] Artur Korniłowicz and Piotr Rudnicki. Fundamental Theorem of Arithmetic. Formalized Mathematics, 12(2):179-186, 2004.
[24] Jarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269-272, 1990.
[25] Jarosław Kotowicz. Convergent sequences and the limit of sequences. Formalized Mathematics, 1(2):273-275, 1990.
[26] Rafał Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887-890, 1990.
[27] Rafał Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relatively primes. Formalized Mathematics, 1(5):829-832, 1990.
[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] Robert Milewski. Natural numbers. Formalized Mathematics, 7(1):19-22, 1998.
[30] Adam Naumowicz. Conjugate sequences, bounded complex sequences and convergent complex sequences. Formalized Mathematics, 6(2):265-268, 1997.
[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] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147-152, 1990.
[33] Konrad Raczkowski and Andrzej Nedzusiak. Series. Formalized Mathematics, 2(4):449-452, 1991.
[34] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25-34, 1990.
[35] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1 (2):329-334, 1990.
[36] Andrzej Trybulec. On the sets inhabited by numbers. Formalized Mathematics, 11(4): 341-347, 2003.
[37] Andrzej Trybulec. Many sorted sets. Formalized Mathematics, 4(1):15-22, 1993.
[38] Andrzej Trybulec and Czesław Bylinski. Some properties of real numbers. Formalized Mathematics, 1(3):445-449, 1990.
[39] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990.
[40] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
[41] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990.
[42] Stanisław Zukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215-222, 1990.