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 * π) * complex.I) * (i / n)) = ζ

theorem complex.mem_roots_of_unity (n : ℕ+) (x : units ) :
x roots_of_unity n ∃ (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.