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 complexn
-th roots of unity are exactly the complex numbers of the forme ^ (2 * real.pi * complex.I * (i / n))
for somei < n
.complex.card_roots_of_unity
: the number ofn
-th roots of unity is exactlyn
.
theorem
complex.is_primitive_root_exp
(n : ℕ)
(h0 : n ≠ 0) :
is_primitive_root (complex.exp ((2 * ↑π) * complex.I / ↑n)) n