REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/3684
Pełny rekord metadanych
Pole DCWartośćJęzyk
dc.contributor.authorGrabowski, Adam-
dc.date.accessioned2015-12-09T20:39:35Z-
dc.date.available2015-12-09T20:39:35Z-
dc.date.issued2013-
dc.identifier.citationFormalized Mathematics, Volume 21, Issue 2, 2013, Pages 153-162-
dc.identifier.issn1426-2630-
dc.identifier.issn1898-9934-
dc.identifier.urihttp://hdl.handle.net/11320/3684-
dc.description.abstractIn 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.-
dc.language.isoen-
dc.publisherDe Gruyter Open-
dc.subjectsquare-free numbers-
dc.subjectprime reciprocals-
dc.subjectlattice of natural divisors-
dc.titleOn Square-Free Numbers-
dc.typeArticle-
dc.identifier.doi10.2478/forma-2013-0017-
dc.description.AffiliationInstitute of Informatics University of Białystok Akademicka 2, 15-267 Białystok Poland-
dc.description.referencesM. Aigner and G. M. Ziegler. Proofs from THE BOOK. Springer-Verlag, Berlin Heidelberg New York, 2004.-
dc.description.referencesGrzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990.-
dc.description.referencesGrzegorz Bancerek. König’s theorem. Formalized Mathematics, 1(3):589-593, 1990.-
dc.description.referencesGrzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990.-
dc.description.referencesGrzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990.-
dc.description.referencesGrzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990.-
dc.description.referencesJózef Białas. Group and field definitions. Formalized Mathematics, 1(3):433-439, 1990.-
dc.description.referencesCzesław Bylinski. Binary operations. Formalized Mathematics, 1(1):175-180, 1990.-
dc.description.referencesCzesław Bylinski. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529-536, 1990.-
dc.description.referencesCzesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990.-
dc.description.referencesCzesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.-
dc.description.referencesCzesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990.-
dc.description.referencesCzesław Bylinski. The sum and product of finite sequences of real numbers. Formalized Mathematics, 1(4):661-668, 1990.-
dc.description.referencesCzesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.-
dc.description.referencesMarek Chmur. The lattice of natural numbers and the sublattice of it. The set of prime numbers. Formalized Mathematics, 2(4):453-459, 1991.-
dc.description.referencesAgata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990.-
dc.description.referencesYoshinori 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.-
dc.description.referencesG.H. Hardy and E.M. Wright. An Introduction to the Theory of Numbers. Oxford University Press, 1980.-
dc.description.referencesMagdalena Jastrzębska 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.-
dc.description.referencesAndrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5): 841-845, 1990.-
dc.description.referencesAndrzej Kondracki. The Chinese Remainder Theorem. Formalized Mathematics, 6(4): 573-577, 1997.-
dc.description.referencesArtur Korniłowicz. On the real valued functions. Formalized Mathematics, 13(1):181-187, 2005.-
dc.description.referencesArtur Korniłowicz and Piotr Rudnicki. Fundamental Theorem of Arithmetic. Formalized Mathematics, 12(2):179-186, 2004.-
dc.description.referencesJarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269-272, 1990.-
dc.description.referencesJarosław Kotowicz. Convergent sequences and the limit of sequences. Formalized Mathematics, 1(2):273-275, 1990.-
dc.description.referencesRafał Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887-890, 1990.-
dc.description.referencesRafał Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relatively primes. Formalized Mathematics, 1(5):829-832, 1990.-
dc.description.referencesXiquan 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.-
dc.description.referencesRobert Milewski. Natural numbers. Formalized Mathematics, 7(1):19-22, 1998.-
dc.description.referencesAdam Naumowicz. Conjugate sequences, bounded complex sequences and convergent complex sequences. Formalized Mathematics, 6(2):265-268, 1997.-
dc.description.referencesHiroyuki 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.-
dc.description.referencesBeata Padlewska. Families of sets. Formalized Mathematics, 1(1):147-152, 1990.-
dc.description.referencesKonrad Raczkowski and Andrzej Nedzusiak. Series. Formalized Mathematics, 2(4):449-452, 1991.-
dc.description.referencesAndrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25-34, 1990.-
dc.description.referencesAndrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1 (2):329-334, 1990.-
dc.description.referencesAndrzej Trybulec. On the sets inhabited by numbers. Formalized Mathematics, 11(4): 341-347, 2003.-
dc.description.referencesAndrzej Trybulec. Many sorted sets. Formalized Mathematics, 4(1):15-22, 1993.-
dc.description.referencesAndrzej Trybulec and Czesław Bylinski. Some properties of real numbers. Formalized Mathematics, 1(3):445-449, 1990.-
dc.description.referencesMichał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990.-
dc.description.referencesZinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.-
dc.description.referencesEdmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990.-
dc.description.referencesStanisław Zukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215-222, 1990.-
Występuje w kolekcji(ach):Artykuły naukowe (WInf)
Formalized Mathematics, 2013, Volume 21, Issue 2

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma-2013-0017.pdf255,61 kBAdobe PDFOtwórz
Pokaż uproszczony widok rekordu Zobacz statystyki


Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons