feat(analysis/complex/roots_of_unity): complex (primitive) roots of u…

…nity (#4330)

docs/undergrad.yaml

@@ -93,8 +93,8 @@ Group Theory:
   Abelian group:
     cyclic group: 'is_cyclic'
     finite type abelian groups: ''
-    complex roots of unity: ''
-    primitive complex roots of unity: ''
+    complex roots of unity: 'complex.mem_roots_of_unity'
+    primitive complex roots of unity: 'complex.is_primitive_root_iff'
   Permutation group:
     permutation group of a type: 'equiv.perm'
     decomposition into transpositions: ''

src/analysis/complex/roots_of_unity.lean

@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2020 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+
+import ring_theory.roots_of_unity
+import analysis.special_functions.trigonometric
+import analysis.special_functions.pow
+
+/-!
+# Complex roots of unity
+
+In this file we show that the `n`-th complex roots of unity
+are exactly the complex numbers `e ^ (2 * real.pi * complex.I * (i / n))` for `i ∈ finset.range n`.
+
+## Main declarations
+
+* `complex.mem_roots_of_unity`: the complex `n`-th roots of unity are exactly the
+  complex numbers of the form `e ^ (2 * real.pi * complex.I * (i / n))` for some `i < n`.
+* `complex.card_roots_of_unity`: the number of `n`-th roots of unity is exactly `n`.
+
+-/
+
+namespace complex
+
+open polynomial real
+open_locale nat
+
+lemma is_primitive_root_exp_of_coprime (i n : ℕ) (h0 : n ≠ 0) (hi : i.coprime n) :
+  is_primitive_root (exp (2 * pi * I * (i / n))) n :=
+begin
+  rw is_primitive_root.iff_def,
+  simp only [← exp_nat_mul, exp_eq_one_iff],
+  have hn0 : (n : ℂ) ≠ 0, by exact_mod_cast h0,
+  split,
+  { use i,
+    field_simp [hn0, mul_comm (i : ℂ), mul_comm (n : ℂ)] },
+  { simp only [hn0, mul_right_comm _ _ ↑n, mul_left_inj' two_pi_I_ne_zero, ne.def, not_false_iff,
+      mul_comm _ (i : ℂ), ← mul_assoc _ (i : ℂ), exists_imp_distrib] with field_simps,
+    norm_cast,
+    rintro l k hk,
+    have : n ∣ i * l,
+    { rw [← int.coe_nat_dvd, hk], apply dvd_mul_left },
+    exact hi.symm.dvd_of_dvd_mul_left this }
+end
+
+lemma is_primitive_root_exp (n : ℕ) (h0 : n ≠ 0) : is_primitive_root (exp (2 * pi * I / n)) n :=
+by simpa only [nat.cast_one, one_div]
+  using is_primitive_root_exp_of_coprime 1 n h0 n.coprime_one_left
+
+lemma is_primitive_root_iff (ζ : ℂ) (n : ℕ) (hn : n ≠ 0) :
+  is_primitive_root ζ n ↔ (∃ (i < (n : ℕ)) (hi : i.coprime n), exp (2 * pi * I * (i / n)) = ζ) :=
+begin
+  have hn0 : (n : ℂ) ≠ 0 := by exact_mod_cast hn,
+  split, swap,
+  { rintro ⟨i, -, hi, rfl⟩, exact is_primitive_root_exp_of_coprime i n hn hi },
+  intro h,
+  obtain ⟨i, hi, rfl⟩ :=
+    (is_primitive_root_exp n hn).eq_pow_of_pow_eq_one h.pow_eq_one (nat.pos_of_ne_zero hn),
+  refine ⟨i, hi, ((is_primitive_root_exp n hn).pow_iff_coprime (nat.pos_of_ne_zero hn) i).mp h, _⟩,
+  rw [← exp_nat_mul],
+  congr' 1,
+  field_simp [hn0, mul_comm (i : ℂ)]
+end
+
+/-- The complex `n`-th roots of unity are exactly the
+complex numbers of the form `e ^ (2 * real.pi * complex.I * (i / n))` for some `i < n`. -/
+lemma mem_roots_of_unity (n : ℕ+) (x : units ℂ) :
+  x ∈ roots_of_unity n ℂ ↔ (∃ i < (n : ℕ), exp (2 * pi * I * (i / n)) = x) :=
+begin
+  rw [mem_roots_of_unity, units.ext_iff, units.coe_pow, units.coe_one],
+  have hn0 : (n : ℂ) ≠ 0 := by exact_mod_cast (n.ne_zero),
+  split,
+  { intro h,
+    obtain ⟨i, hi, H⟩ : ∃ i < (n : ℕ), exp (2 * pi * I / n) ^ i = x,
+    { simpa only using (is_primitive_root_exp n n.ne_zero).eq_pow_of_pow_eq_one h n.pos },
+    refine ⟨i, hi, _⟩,
+    rw [← H, ← exp_nat_mul],
+    congr' 1,
+    field_simp [hn0, mul_comm (i : ℂ)] },
+  { rintro ⟨i, hi, H⟩,
+    rw [← H, ← exp_nat_mul, exp_eq_one_iff],
+    use i,
+    field_simp [hn0, mul_comm ((n : ℕ) : ℂ), mul_comm (i : ℂ)] }
+end
+
+lemma card_roots_of_unity (n : ℕ+) : fintype.card (roots_of_unity n ℂ) = n :=
+(is_primitive_root_exp n n.ne_zero).card_roots_of_unity
+
+lemma card_primitive_roots (k : ℕ) (h : k ≠ 0) : (primitive_roots k ℂ).card = φ k :=
+(is_primitive_root_exp k h).card_primitive_roots (nat.pos_of_ne_zero h)
+
+end complex

src/analysis/special_functions/trigonometric.lean

@@ -571,6 +571,9 @@ lemma pi_le_four : π ≤ 4 :=
 lemma pi_pos : 0 < π :=
 lt_of_lt_of_le (by norm_num) two_le_pi
 
+lemma pi_ne_zero : pi ≠ 0 :=
+ne_of_gt pi_pos
+
 lemma pi_div_two_pos : 0 < π / 2 :=
 half_pos pi_pos
 
@@ -1604,6 +1607,9 @@ lemma log_I : log I = π / 2 * I := by simp [log]
 
 lemma log_neg_I : log (-I) = -(π / 2) * I := by simp [log]
 
+lemma two_pi_I_ne_zero : (2 * π * I : ℂ) ≠ 0 :=
+by norm_num [real.pi_ne_zero, I_ne_zero]
+
 lemma exp_eq_one_iff {x : ℂ} : exp x = 1 ↔ ∃ n : ℤ, x = n * ((2 * π) * I) :=
 have real.exp (x.re) * real.cos (x.im) = 1 → real.cos x.im ≠ -1,
   from λ h₁ h₂, begin