English
If a real angle θ is a rational multiple of π and cos θ is rational, then cos θ can only be one of -1, -1/2, 0, 1/2, 1.
Русский
Если угол θ является рациональным кратным π и cos θ рационален, то cos θ может принимать только значения -1, -1/2, 0, 1/2, 1.
LaTeX
$$$\\forall θ\\in\\mathbb{R},\\ (\\exists r\\in\\mathbb{Q}, θ=r\\pi) \\land (\\exists q\\in\\mathbb{Q},\\cos θ=q) \\Rightarrow \\cos θ \\in \\{-1,-\\tfrac12,0,\\tfrac12,1\\}$$$
Lean4
/-- **Niven's theorem**: The only rational values of `cos` that occur at rational multiples of π
are `{-1, -1/2, 0, 1/2, 1}`. -/
theorem niven (hθ : ∃ r : ℚ, θ = r * π) (hcos : ∃ q : ℚ, cos θ = q) : cos θ ∈ ({-1, -1 / 2, 0, 1 / 2, 1} : Set ℝ) := by
-- Since `2 cos θ ` is an algebraic integer and rational, it must be an integer.
-- Hence, `2 cos θ ∈ {-2, -1, 0, 1, 2}`.
obtain ⟨r, rfl⟩ := hθ
obtain ⟨k, hk⟩ : ∃ k : ℤ, 2 * cos (r * π) = k :=
by
rw [← (isIntegral_two_mul_cos_rat_mul_pi r).exists_int_iff_exists_rat]
exact
⟨2 * hcos.choose, by push_cast; linarith [hcos.choose_spec]⟩
-- Since k is an integer and `2 * cos (w * pi) = k`, we have $k ∈ {-2, -1, 0, 1, 2}$.
have hk_values : k ∈ Finset.Icc (-2 : ℤ) 2 := by
rw [Finset.mem_Icc]
rify
constructor <;> linarith [hk, (r * π).neg_one_le_cos, (r * π).cos_le_one]
rw [show cos (r * π) = k / 2 by grind]
fin_cases hk_values <;> simp
