Geometric Sum of Primitive Root Powers

 Complex.exp (2 * π * Complex.I / N)
    ∑ k ∈ Finset.range N, ω ^ (k * m) = 0 := by
  intro ω
  have hN' : N ≠ 0 := Nat.pos_iff_ne_zero.mp hN
  have hω : IsPrimitiveRoot ω N := Complex.isPrimitiveRoot_exp N hN'
  conv_lhs => arg 2; ext k; rw [mul_comm k m, pow_mul]
  have h_ne_one : ω ^ m ≠ 1 := by
    intro h_eq
    have h_div : N ∣ m := (hω.pow_eq_one_iff_dvd m).mp h_eq
    have : N ≤ m := Nat.le_of_dvd hm h_div
    omega
  have h_pow_N : (ω ^ m) ^ N = 1 := by
    calc (ω ^ m) ^ N = ω ^ (m * N) := by rw [← pow_mul]
      _ = ω ^ (N * m) := by rw [mul_comm]
      _ = (ω ^ N) ^ m := by rw [← pow_mul]
      _ = 1 ^ m := by rw [hω.pow_eq_one]
      _ = 1 := one_pow m
  have h_geom : (ω ^ m - 1) * ∑ k ∈ Finset.range N, (ω ^ m) ^ k = (ω ^ m) ^ N - 1 :=
    mul_geom_sum (ω ^ m) N
  rw [h_pow_N] at h_geom
  have h_eq_zero : (ω ^ m - 1) * ∑ k ∈ Finset.range N, (ω ^ m) ^ k = 0 := by
    rw [h_geom]; ring
  exact eq_zero_of_ne_zero_of_mul_left_eq_zero (sub_ne_zero_of_ne h_ne_one) h_eq_zero