# mathlib3documentation

ring_theory.roots_of_unity.complex

# Complex roots of unity #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.
theorem complex.is_primitive_root_exp_of_coprime (i n : ) (h0 : n 0) (hi : i.coprime n) :
theorem complex.is_primitive_root_iff (ζ : ) (n : ) (hn : n 0) :
(i : ) (H : i < n) (hi : i.coprime n), cexp * (i / n)) = ζ
theorem complex.mem_roots_of_unity (n : ℕ+) (x : ˣ) :
x (i : ) (H : i < n), cexp * (i / n)) = x

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.

theorem is_primitive_root.norm'_eq_one {ζ : } {n : } (h : n) (hn : n 0) :
ζ = 1
theorem is_primitive_root.nnnorm_eq_one {ζ : } {n : } (h : n) (hn : n 0) :
theorem is_primitive_root.arg_ext {n m : } {ζ μ : } (hζ : n) (hμ : m) (hn : n 0) (hm : m 0) (h : ζ.arg = μ.arg) :
ζ = μ
theorem is_primitive_root.arg_eq_zero_iff {n : } {ζ : } (hζ : n) (hn : n 0) :
ζ.arg = 0 ζ = 1
theorem is_primitive_root.arg_eq_pi_iff {n : } {ζ : } (hζ : n) (hn : n 0) :
ζ = -1
theorem is_primitive_root.arg {n : } {ζ : } (h : n) (hn : n 0) :
(i : ), ζ.arg = i / n * (2 * real.pi) n i.nat_abs < n