mathlib documentation

analysis.complex.roots_of_unity

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 #

theorem complex.is_primitive_root_iff (ζ : ) (n : ) (hn : n 0) :
is_primitive_root ζ n ∃ (i : ) (H : i < n) (hi : i.coprime n), complex.exp (2 * real.pi * complex.I * (i / n)) = ζ
theorem complex.mem_roots_of_unity (n : ℕ+) (x : ˣ) :
x roots_of_unity n ∃ (i : ) (H : i < n), complex.exp (2 * real.pi * complex.I * (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 : is_primitive_root ζ n) (hn : n 0) :
ζ = 1
theorem is_primitive_root.nnnorm_eq_one {ζ : } {n : } (h : is_primitive_root ζ n) (hn : n 0) :
theorem is_primitive_root.arg_ext {n m : } {ζ μ : } (hζ : is_primitive_root ζ n) (hμ : is_primitive_root μ m) (hn : n 0) (hm : m 0) (h : ζ.arg = μ.arg) :
ζ = μ
theorem is_primitive_root.arg_eq_zero_iff {n : } {ζ : } (hζ : is_primitive_root ζ n) (hn : n 0) :
ζ.arg = 0 ζ = 1
theorem is_primitive_root.arg_eq_pi_iff {n : } {ζ : } (hζ : is_primitive_root ζ n) (hn : n 0) :
ζ.arg = real.pi ζ = -1
theorem is_primitive_root.arg {n : } {ζ : } (h : is_primitive_root ζ n) (hn : n 0) :
∃ (i : ), ζ.arg = i / n * (2 * real.pi) is_coprime i n i.nat_abs < n