Niven's Theorem

This file proves Niven's theorem, stating that the only rational angles in degrees which also have rational cosines, are 0, 30 degrees, and 90 degrees - up to reflection and shifts by π. Equivalently, the only rational numbers that occur as cos(π * p / q) are the five values {-1, -1/2, 0, 1/2, 1}.

@[simp]

theorem IsIntegral.ratCast_iff {α : Type u_1} [DivisionRing α] [CharZero α] {q : ℚ} : IsIntegral ℤ ↑q ↔ IsIntegral ℤ q

theorem IsIntegral.exists_int_iff_exists_rat {α : Type u_1} [DivisionRing α] [CharZero α] {x : α} (h₁ : IsIntegral ℤ x) : (∃ (q : ℚ), x = ↑q) ↔ ∃ (k : ℤ), x = ↑k

theorem isIntegral_two_mul_cos_rat_mul_pi (r : ℚ) : IsIntegral ℤ (2 * Real.cos (↑r * Real.pi))

theorem niven {θ : ℝ} (hθ : ∃ (r : ℚ), θ = ↑r * Real.pi) (hcos : ∃ (q : ℚ), Real.cos θ = ↑q) : Real.cos θ ∈ {-1, -1 / 2, 0, 1 / 2, 1}

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_sin {θ : ℝ} (hθ : ∃ (r : ℚ), θ = ↑r * Real.pi) (hcos : ∃ (q : ℚ), Real.sin θ = ↑q) : Real.sin θ ∈ {-1, -1 / 2, 0, 1 / 2, 1}

Niven's theorem, but stated for sin instead of cos.

theorem niven_angle_eq {θ : ℝ} (hθ : ∃ (r : ℚ), θ = ↑r * Real.pi) (hcos : ∃ (q : ℚ), Real.cos θ = ↑q) (h_bnd : θ ∈ Set.Icc 0 Real.pi) : θ ∈ {0, Real.pi / 3, Real.pi / 2, Real.pi * (2 / 3), Real.pi}

Niven's theorem, giving the possible angles for θ in the range 0 .. π.