[Merged by Bors] - feat(Analysis/SpecialFunctions/Complex/Log): natural number versions of exp_eq_one_iff

Mathlib/Analysis/SpecialFunctions/Complex/Log.lean

@@ -149,6 +149,26 @@ theorem exp_eq_one_iff {x : ℂ} : exp x = 1 ↔ ∃ n : ℤ, x = n * (2 * π *
   · rintro ⟨n, rfl⟩
     exact (exp_periodic.int_mul n).eq.trans exp_zero
 
+theorem exp_eq_one_iff_of_im_nonneg {x : ℂ} (hx : 0 ≤ x.im) :
+    exp x = 1 ↔ ∃ n : ℕ, x = n * (2 * π * I) := by
+  rw [exp_eq_one_iff]
+  refine ⟨fun ⟨n, hn⟩ ↦ ?_, fun ⟨n, hn⟩ ↦ ⟨n, by rw [hn]; norm_cast⟩⟩
+  lift n to ℕ
+  · rw [hn] at hx
+    rw [show (n * (2 * ↑π * I) : ℂ).im = n * (2 * π) by simp] at hx
+    exact_mod_cast nonneg_of_mul_nonneg_left hx (mul_pos two_pos Real.pi_pos)
+  · exact ⟨n, hn⟩
+
+theorem exp_two_pi_mul_I_mul_div_eq_one_iff {k N : ℕ} (hN : N ≠ 0) :
+    exp (2 * π * I * k / N) = 1 ↔ N ∣ k := by
+  have hN' : (N : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr hN
+  rw [exp_eq_one_iff]
+  refine ⟨fun ⟨n, hn⟩ ↦ ?_, fun ⟨m, hm⟩ ↦ ⟨m, by rw [hm]; push_cast; field_simp⟩⟩
+  suffices k = n * N by exact Int.ofNat_dvd.1 ⟨n, by grind⟩
+  have h0 : 2 * π * I ≠ 0 := by simp
+  refine Int.cast_inj.1 ((mul_left_inj' h0).1 ?_)
+  grind [Int.cast_natCast]
+
 theorem exp_eq_exp_iff_exp_sub_eq_one {x y : ℂ} : exp x = exp y ↔ exp (x - y) = 1 := by
   rw [exp_sub, div_eq_one_iff_eq (exp_ne_zero _)]