Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/5564
Pełny rekord metadanych
Pole DC | Wartość | Język |
---|---|---|
dc.contributor.author | Korniłowicz, Artur | - |
dc.contributor.author | Naumowicz, Adam | - |
dc.date.accessioned | 2017-06-02T11:55:31Z | - |
dc.date.available | 2017-06-02T11:55:31Z | - |
dc.date.issued | 2016 | - |
dc.identifier.citation | Formalized Mathematics, Volume 24, Issue 4, pp. 301-308 | pl |
dc.identifier.issn | 1426-2630 | pl |
dc.identifier.issn | 1898-9934 | pl |
dc.identifier.uri | http://hdl.handle.net/11320/5564 | - |
dc.description.abstract | This article formalizes the proof of Niven’s theorem [12] which states that if x/π and sin(x) are both rational, then the sine takes values 0, ±1/2, and ±1. The main part of the formalization follows the informal proof presented at Pr∞fWiki (https://proofwiki.org/wiki/Niven’s_Theorem#Source_of_Name). For this proof, we have also formalized the rational and integral root theorems setting constraints on solutions of polynomial equations with integer coefficients [8, 9]. | - |
dc.language.iso | en | - |
dc.publisher | De Gruyter Open | - |
dc.subject | Niven’s theorem | - |
dc.subject | rational root theorem | - |
dc.subject | integral root theorem | - |
dc.title | Niven’s Theorem | - |
dc.type | Article | - |
dc.identifier.doi | 10.1515/forma-2016-0026 | - |
dc.description.Affiliation | Korniłowicz Artur - Institute of Informatics, University of Białystok, Poland | - |
dc.description.Affiliation | Naumowicz Adam - Institute of Informatics, University of Białystok, Poland | - |
dc.description.references | Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990. | - |
dc.description.references | Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990. | - |
dc.description.references | Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Formalized Mathematics, 5(4):485–492, 1996. | - |
dc.description.references | Czesław Byliński. The sum and product of finite sequences of real numbers. Formalized Mathematics, 1(4):661–668, 1990. | - |
dc.description.references | Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990. | - |
dc.description.references | Yuzhong Ding and Xiquan Liang. Formulas and identities of trigonometric functions. Formalized Mathematics, 12(3):243–246, 2004. | - |
dc.description.references | Magdalena Jastrzębska and Adam Grabowski. Some properties of Fibonacci numbers. Formalized Mathematics, 12(3):307–313, 2004. | - |
dc.description.references | J.D. King. Integer roots of polynomials. The Mathematical Gazette, 90(519):455–456, 2006. doi:http://dx.doi.org/10.1017/S0025557200180295. | - |
dc.description.references | Serge Lang. Algebra. Addison-Wesley, 1980. | - |
dc.description.references | Robert Milewski. The evaluation of polynomials. Formalized Mathematics, 9(2):391–395, 2001. | - |
dc.description.references | Robert Milewski. Fundamental theorem of algebra. Formalized Mathematics, 9(3):461–470, 2001. | - |
dc.description.references | Ivan Niven. Irrational numbers. The Carus Mathematical Monographs, No. 11. The Mathematical Association of America. Distributed by John Wiley and Sons, Inc., New York, N.Y., 1956. | - |
dc.description.references | Piotr Rudnicki. Little Bezout theorem (factor theorem). Formalized Mathematics, 12(1): 49–58, 2004. | - |
dc.description.references | Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1 (2):329–334, 1990. | - |
dc.description.references | Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501–505, 1990. | - |
dc.description.references | Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291–296, 1990. | - |
Występuje w kolekcji(ach): | Artykuły naukowe (WInf) Formalized Mathematics, 2016, Volume 24, Issue 4 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
forma-2016-0026.pdf | 261,76 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL