Niven’s Theorem

Artur Korniłowicz, and Adam Naumowicz. "Niven’s Theorem." Formalized Mathematics 24.4 (2016): 301-308. <http://eudml.org/doc/287983>.

@article{ArturKorniłowicz2016,
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].},
author = {Artur Korniłowicz, Adam Naumowicz},
journal = {Formalized Mathematics},
keywords = {Niven’s theorem; rational root theorem; integral root theorem; Niven's theorem},
language = {eng},
number = {4},
pages = {301-308},
title = {Niven’s Theorem},
url = {http://eudml.org/doc/287983},
volume = {24},
year = {2016},
}

TY - JOUR
AU - Artur Korniłowicz
AU - Adam Naumowicz
TI - Niven’s Theorem
JO - Formalized Mathematics
PY - 2016
VL - 24
IS - 4
SP - 301
EP - 308
AB - 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].
LA - eng
KW - Niven’s theorem; rational root theorem; integral root theorem; Niven's theorem
UR - http://eudml.org/doc/287983
ER -