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 Complex.exp_rat_mul_pi_mul_I_pow_two_mul_den (q : ℚ) : exp (↑q * ↑Real.pi * I) ^ (2 * q.den) = 1

theorem Complex.isIntegral_exp_rat_mul_pi_mul_I (q : ℚ) : IsIntegral ℤ (exp (↑q * ↑Real.pi * I))

exp(q * π * I) for q : ℚ is integral over ℤ.

theorem Complex.isIntegral_exp_neg_rat_mul_pi_mul_I (q : ℚ) : IsIntegral ℤ (exp (-(↑q * ↑Real.pi) * I))

exp(-(q * π) * I) for q : ℚ is integral over ℤ.

theorem Complex.isIntegral_two_mul_sin_rat_mul_pi (q : ℚ) : IsIntegral ℤ (2 * sin (↑q * ↑Real.pi))

2 sin(q * π) for q : ℚ is integral over ℤ, using the complex sin function.

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

2 cos(q * π) for q : ℚ is integral over ℤ, using the complex cos function.

theorem Complex.isAlgebraic_sin_rat_mul_pi (q : ℚ) : IsAlgebraic ℤ (sin (↑q * ↑Real.pi))

sin(q * π) for q : ℚ is algebraic over ℤ, using the complex sin function.

theorem Complex.isAlgebraic_cos_rat_mul_pi (q : ℚ) : IsAlgebraic ℤ (cos (↑q * ↑Real.pi))

cos(q * π) for q : ℚ is algebraic over ℤ, using the complex cos function.

theorem Complex.isAlgebraic_tan_rat_mul_pi (q : ℚ) : IsAlgebraic ℤ (tan (↑q * ↑Real.pi))

tan(q * π) for q : ℚ is algebraic over ℤ, using the complex tan function.

theorem Real.isIntegral_two_mul_sin_rat_mul_pi (q : ℚ) : IsIntegral ℤ (2 * sin (↑q * Real.pi))

2 sin(q * π) for q : ℚ is integral over ℤ, using the real sin function.

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

2 cos(q * π) for q : ℚ is integral over ℤ, using the real cos function.

@[deprecated Real.isIntegral_two_mul_cos_rat_mul_pi (since := "2025-11-15")]

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

Alias of Real.isIntegral_two_mul_cos_rat_mul_pi.

---

2 cos(q * π) for q : ℚ is integral over ℤ, using the real cos function.

theorem Real.isAlgebraic_sin_rat_mul_pi (q : ℚ) : IsAlgebraic ℤ (sin (↑q * Real.pi))

sin(q * π) for q : ℚ is algebraic over ℤ, using the real sin function.

theorem Real.isAlgebraic_cos_rat_mul_pi (q : ℚ) : IsAlgebraic ℤ (cos (↑q * Real.pi))

cos(q * π) for q : ℚ is algebraic over ℤ, using the real cos function.

theorem Real.isAlgebraic_tan_rat_mul_pi (q : ℚ) : IsAlgebraic ℤ (tan (↑q * Real.pi))

tan(q * π) for q : ℚ is algebraic over ℤ, using the real tan function.

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

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

theorem niven_fract_angle_div_pi_eq {r : ℚ} (hcos : ∃ (q : ℚ), Real.cos (↑r * Real.pi) = ↑q) : Int.fract r ∈ {0, 1 / 3, 1 / 2, 2 / 3}

theorem irrational_cos_rat_mul_pi {r : ℚ} (hr : 3 < r.den) : Irrational (Real.cos (↑r * Real.pi))