Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
Pełny rekord metadanych
Pole DCWartośćJęzyk
dc.contributor.authorZiobro, Rafałpl
dc.identifier.citationFormalized Mathematics, Volume 23, Issue 3, 215–229pl
dc.description.abstractAbstractSolving equations in integers is an important part of the number theory [29]. In many cases it can be conducted by the factorization of equation’s elements, such as the Newton’s binomial. The article introduces several simple formulas, which may facilitate this process. Some of them are taken from relevant books [28], [14]. In the second section of the article, Fermat’s Little Theorem is proved in a classical way, on the basis of divisibility of Newton’s binomial. Although slightly redundant in its content (another proof of the theorem has earlier been included in [12]), the article provides a good example, how the application of registrations could shorten the length of Mizar proofs [9], [17].pl
dc.publisherDe Gruyter Openpl
dc.titleFermat’s Little Theorem via Divisibility of Newton’s Binomialpl
dc.description.AffiliationDepartment of Carbohydrate Technology, University of Agriculture, Krakow, Polandpl
dc.description.referencesGrzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382,
dc.description.referencesGrzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46,
dc.description.referencesGrzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96,
dc.description.referencesGrzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114,
dc.description.referencesCzesław Bylinski. The complex numbers. Formalized Mathematics, 1(3):507-513,
dc.description.referencesCzesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65,
dc.description.referencesCzesław Bylinski. The sum and product of finite sequences of real numbers. Formalized Mathematics, 1(4):661-668,
dc.description.referencesCzesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53,
dc.description.referencesMarco B. Caminati and Giuseppe Rosolini. Custom automations in Mizar. Journal of Automated Reasoning, 50(2):147-160,
dc.description.referencesAgata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167,
dc.description.referencesYoshinori Fujisawa and Yasushi Fuwa. The Euler’s function. Formalized Mathematics, 6 (4):549-551,
dc.description.referencesYoshinori Fujisawa, Yasushi Fuwa, and Hidetaka Shimizu. Euler’s Theorem and small Fermat’s Theorem. Formalized Mathematics, 7(1):123-126,
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,
dc.description.referencesJacek Gancarzewicz. Arytmetyka, 2000. In
dc.description.referencesKrzysztof Hryniewiecki. Recursive definitions. Formalized Mathematics, 1(2):321-328,
dc.description.referencesAndrzej Kondracki. The Chinese Remainder Theorem. Formalized Mathematics, 6(4): 573-577,
dc.description.referencesArtur Korniłowicz. On rewriting rules in Mizar. Journal of Automated Reasoning, 50(2): 203-210,
dc.description.referencesArtur Korniłowicz and Piotr Rudnicki. Fundamental Theorem of Arithmetic. Formalized Mathematics, 12(2):179-186,
dc.description.referencesJarosław Kotowicz. Functions and finite sequences of real numbers. Formalized Mathematics, 3(2):275-278,
dc.description.referencesRichard Krueger, Piotr Rudnicki, and Paul Shelley. Asymptotic notation. Part II: Examples and problems. Formalized Mathematics, 9(1):143-154,
dc.description.referencesRafał Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887-890,
dc.description.referencesRafał Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relatively primes. Formalized Mathematics, 1(5):829-832,
dc.description.referencesBeata Padlewska. Families of sets. Formalized Mathematics, 1(1):147-152,
dc.description.referencesKonrad Raczkowski. Integer and rational exponents. Formalized Mathematics, 2(1):125-130,
dc.description.referencesKonrad Raczkowski and Andrzej Nedzusiak. Real exponents and logarithms. Formalized Mathematics, 2(2):213-216,
dc.description.referencesPiotr Rudnicki and Andrzej Trybulec. Abian’s fixed point theorem. Formalized Mathematics, 6(3):335-338,
dc.description.referencesChristoph Schwarzweller. Modular integer arithmetic. Formalized Mathematics, 16(3): 247-252, 2008. doi:10.2478/v10037-008-0029-8. [Crossref]pl
dc.description.referencesWacław Sierpinski. Teoria liczb. 1950. In
dc.description.referencesWacław Sierpinski. O rozwiazywaniu rownan w liczbach całkowitych, 1956. In
dc.description.referencesMichał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505,
dc.description.referencesWojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569-573,
dc.description.referencesEdmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83,
dc.description.referencesLi Yan, Xiquan Liang, and Junjie Zhao. Gauss lemma and law of quadratic reciprocity. Formalized Mathematics, 16(1):23-28, 2008. doi:10.2478/v10037-008-0004-4. [Crossref]pl
dc.description.referencesRafał Ziobro. Some remarkable identities involving numbers. Formalized Mathematics, 22(3):205-208, 2014. doi:10.2478/forma-2014-0023. [Crossref]pl
Występuje w kolekcji(ach):Formalized Mathematics, 2015, Volume 23, Issue 3

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma-2015-0018.pdf276,57 kBAdobe PDFOtwórz
Pokaż uproszczony widok rekordu Zobacz statystyki

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