feat(RingTheory/RootsOfUnity/Complex): 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,33 @@ 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
+  convert isPrimitiveRoot_exp_of_coprime _ _ (Int.fract q).den_ne_zero (Int.fract q).reduced using 1
+  · nth_rw 1 [← Int.floor_add_fract q, ← Int.fract q |>.num_div_den]
+    nth_rw 1 [Int.eq_natAbs_of_nonneg <| Int.fract q |>.num_nonneg.mpr <| Int.fract_nonneg _]
+    rw [Rat.cast_add, Rat.cast_intCast, Rat.cast_div, Rat.cast_intCast]
+    simp [mul_add, mul_comm _ (⌊q⌋ : ℂ), Complex.exp_add]
+  · simp [← Rat.add_intCast_den q (-⌊q⌋), ← sub_eq_add_neg]
+
+theorem isPrimitiveRoot_exp_rat_of_even_num (q : ℚ) (h : Even q.num) :
+    IsPrimitiveRoot (exp (π * I * q)) q.den := by
+  have ⟨n, hn⟩ := even_iff_exists_two_nsmul _ |>.mp h
+  convert isPrimitiveRoot_exp_two_rat (n / q.den) using 1
+  · nth_rw 1 [← q.num_div_den, hn]
+    grind [Rat.cast_mul, Rat.cast_ofNat]
+  · rw [← Int.cast_natCast, ← Rat.divInt_eq_div, ← Rat.mk_eq_divInt _ _ (by simp) ?_]
+    apply Nat.Coprime.coprime_mul_left (k := 2)
+    grind [Rat.reduced]
+
+theorem isPrimitiveRoot_exp_rat_of_odd_num (q : ℚ) (h : Odd q.num) :
+    IsPrimitiveRoot (exp (π * I * q)) (2 * q.den) := by
+  convert isPrimitiveRoot_exp_two_rat (q / 2) using 1
+  · grind [Rat.cast_div, Rat.cast_ofNat]
+  · nth_rw 2 [← q.num_div_den]
+    rw [mul_comm, div_div, ← Int.cast_ofNat, ← Int.cast_natCast, ← Int.cast_mul,
+      ← Rat.divInt_eq_div, ← Nat.cast_ofNat (R := ℤ), ← Nat.cast_mul,
+      ← Rat.mk_eq_divInt _ _ (by simp) (Nat.Coprime.mul_right q.reduced h.natAbs.coprime_two_right)]
+
 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