On Square-Free Numbers
Adam Grabowski (2013)
Formalized Mathematics
Similarity:
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...