English
If θ is a rational multiple of π, and sin θ is rational, then sin θ must be among -1, -1/2, 0, 1/2, 1.
Русский
Если θ — рациональное кратное π и sin θ рационален, то sin θ принадлежит набору -1, -1/2, 0, 1/2, 1.
LaTeX
$$$\\forall θ,\\ (\\exists r\\in\\mathbb{Q}, θ=r\\pi) \\land (\\exists q\\in\\mathbb{Q},\\sin θ=q) \\Rightarrow \\sin θ \\in \\{-1,-\\tfrac12,0,\\tfrac12,1\\}$$$
Lean4
/-- Niven's theorem, but stated for `sin` instead of `cos`. -/
theorem niven_sin (hθ : ∃ r : ℚ, θ = r * π) (hcos : ∃ q : ℚ, sin θ = q) : sin θ ∈ ({-1, -1 / 2, 0, 1 / 2, 1} : Set ℝ) :=
by
convert ← niven (θ := θ - π / 2) ?_ ?_ using 1
· exact cos_sub_pi_div_two θ
· exact hθ.imp' (· - 1 / 2) (by intros; push_cast; linarith)
· simpa [cos_sub_pi_div_two]
