# mathlibdocumentation

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 #

• 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_iff (ζ : ) (n : ) (hn : n 0) :
∃ (i : ) (H : i < n) (hi : i.coprime n), complex.exp (((2 * π) * complex.I) * (i / n)) = ζ
theorem complex.mem_roots_of_unity (n : ℕ+) (x : units ) :
x ∃ (i : ) (H : i < n), complex.exp (((2 * π) * 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 complex.card_primitive_roots (k : ) (h : k 0) :