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 * ↑real.pi * complex.I / ↑n)) n
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) :