Niven’s Theorem

• Autorzy: Artur Korniłowicz , Adam Naumowicz
• Języki publikacji: EN

Abstrakty

EN

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].

Słowa kluczowe

EN

Niven’s theorem; rational root theorem; integral root theorem

Kategorie tematyczne

• 03B35: Mechanization of proofs and logical operations
• 97G60: Plane and spherical trigonometry
• 12D10: Polynomials: location of zeros (algebraic theorems)

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2016
• Tom: 24
• Numer: 4
• Strony: 301-308

Daty

wydano

2016-12-01

otrzymano

2016-12-15

online

2017-02-23

Twórcy

autor

Artur Korniłowicz

• Institute of Informatics, University of Białystok,

autor

Adam Naumowicz

• Institute of Informatics, University of Białystok,

Identyfikatory

DOI

10.1515/forma-2016-0026