feat(RingTheory/RootsOfUnity): exp(pi * i * q) is a root of unity for rational q

Author: SnirBroshi

Mathlib/RingTheory/RootsOfUnity/Complex.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johan Commelin
+Authors: Johan Commelin, Snir Broshi
 -/
 import Mathlib.Analysis.SpecialFunctions.Complex.Log
 import Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
@@ -44,6 +44,41 @@ theorem isPrimitiveRoot_exp_of_coprime (i n : ℕ) (h0 : n ≠ 0) (hi : i.Coprim
     have : n ∣ l * i := by rw [← Int.natCast_dvd_natCast, hk]; apply dvd_mul_right
     exact hi.symm.dvd_of_dvd_mul_right this
 
+theorem isPrimitiveRoot_exp_two_rat (q : ℚ) : IsPrimitiveRoot (exp (2 * π * I * q)) q.den := by
+  nth_rw 1 [← Int.floor_add_fract q]
+  push_cast
+  rw [mul_add, Complex.exp_add, mul_comm _ (⌊q⌋ : ℂ), ← (Int.fract q).num_div_den]
+  rw [← Rat.add_intCast_den q (-⌊q⌋)]
+  simp
+  rw [Int.eq_natAbs_of_nonneg <| (Int.fract q).num_nonneg.mpr <| Int.fract_nonneg _]
+  rw [← sub_eq_add_neg]
+  exact isPrimitiveRoot_exp_of_coprime _ _ (Int.fract q).den_ne_zero (Int.fract q).reduced
+
+theorem isPrimitiveRoot_exp_rat_of_even_num (q : ℚ) (h : Even q.num) :
+    IsPrimitiveRoot (exp (π * I * q)) q.den := by
+  have ⟨n, h⟩ := even_iff_exists_two_nsmul _ |>.mp h
+  nth_rw 1 [← q.num_div_den]
+  rw [h]
+  simp
+  rw [show π * I * (2 * n / q.den) = 2 * π * I * (n / (q.den : ℤ) : ℚ) by simp; ring_nf]
+  rw [← Rat.divInt_eq_div]
+  have : q.num.natAbs = 2 * n.natAbs := by grind
+  rw [← Rat.mk_eq_divInt _ _ (by simp) <| Nat.Coprime.coprime_mul_left <| this ▸ q.reduced]
+  exact isPrimitiveRoot_exp_two_rat _
+
+theorem isPrimitiveRoot_exp_rat_of_odd_num (q : ℚ) (h : Odd q.num) :
+    IsPrimitiveRoot (exp (π * I * q)) (2 * q.den) := by
+  have := isPrimitiveRoot_exp_two_rat (q / 2)
+  push_cast at this
+  rw [show 2 * π * I * (q / 2) = π * I * q by ring_nf] at this
+  convert this
+  nth_rw 2 [← q.num_div_den]
+  rw [mul_comm, div_div]
+  rw [show (q.num / (q.den * 2) : ℚ) = q.num / (q.den * 2 : ℤ) by simp]
+  rw [← Rat.divInt_eq_div, show (q.den * 2 : ℤ) = (q.den * 2 : ℕ) by simp]
+  have := Nat.Coprime.mul_right q.reduced h.natAbs.coprime_two_right
+  rw [← Rat.mk_eq_divInt _ _ (by simp) this]
+
 theorem isPrimitiveRoot_exp (n : ℕ) (h0 : n ≠ 0) : IsPrimitiveRoot (exp (2 * π * I / n)) n := by
   simpa only [Nat.cast_one, one_div] using
     isPrimitiveRoot_exp_of_coprime 1 n h0 n.coprime_one_left