# Complex roots of unity #

In this file we show that the n-th complex roots of unity are exactly the complex numbers exp (2 * π * I * (i / n)) for i ∈ Finset.range n.

## Main declarations #

• Complex.mem_rootsOfUnity: the complex n-th roots of unity are exactly the complex numbers of the form exp (2 * π * I * (i / n)) for some i < n.
• Complex.card_rootsOfUnity: the number of n-th roots of unity is exactly n.
• Complex.norm_rootOfUnity_eq_one: A complex root of unity has norm 1.
theorem Complex.isPrimitiveRoot_exp_of_coprime (i : ) (n : ) (h0 : n 0) (hi : i.Coprime n) :
IsPrimitiveRoot (Complex.exp ( * (i / n))) n
theorem Complex.isPrimitiveRoot_iff (ζ : ) (n : ) (hn : n 0) :
i < n, ∃ (_ : i.Coprime n), Complex.exp ( * (i / n)) = ζ
theorem Complex.mem_rootsOfUnity (n : ℕ+) (x : ) :
x i < n, Complex.exp ( * (i / n)) = x

The complex n-th roots of unity are exactly the complex numbers of the form exp (2 * Real.pi * Complex.I * (i / n)) for some i < n.

theorem Complex.card_primitiveRoots (k : ) :
().card = k.totient
theorem IsPrimitiveRoot.norm'_eq_one {ζ : } {n : } (h : ) (hn : n 0) :
ζ = 1
theorem IsPrimitiveRoot.nnnorm_eq_one {ζ : } {n : } (h : ) (hn : n 0) :
theorem IsPrimitiveRoot.arg_ext {n : } {m : } {ζ : } {μ : } (hζ : ) (hμ : ) (hn : n 0) (hm : m 0) (h : ζ.arg = μ.arg) :
ζ = μ
theorem IsPrimitiveRoot.arg_eq_zero_iff {n : } {ζ : } (hζ : ) (hn : n 0) :
ζ.arg = 0 ζ = 1
theorem IsPrimitiveRoot.arg_eq_pi_iff {n : } {ζ : } (hζ : ) (hn : n 0) :
ζ.arg = Real.pi ζ = -1
theorem IsPrimitiveRoot.arg {n : } {ζ : } (h : ) (hn : n 0) :
∃ (i : ), ζ.arg = i / n * () IsCoprime i n i.natAbs < n
theorem Complex.norm_eq_one_of_mem_rootsOfUnity {ζ : } {n : ℕ+} (hζ : ζ ) :
ζ = 1