Documentation

Mathlib.RingTheory.RootsOfUnity.Complex

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 #

theorem Complex.isPrimitiveRoot_exp_of_coprime (i : ) (n : ) (h0 : n 0) (hi : Nat.Coprime i n) :
theorem Complex.isPrimitiveRoot_iff (ζ : ) (n : ) (hn : n 0) :
IsPrimitiveRoot ζ n i, i < n x, Complex.exp (2 * Real.pi * Complex.I * (i / n)) = ζ
theorem Complex.mem_rootsOfUnity (n : ℕ+) (x : ˣ) :
x rootsOfUnity n i, i < n Complex.exp (2 * Real.pi * Complex.I * (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 IsPrimitiveRoot.norm'_eq_one {ζ : } {n : } (h : IsPrimitiveRoot ζ n) (hn : n 0) :
ζ = 1
theorem IsPrimitiveRoot.nnnorm_eq_one {ζ : } {n : } (h : IsPrimitiveRoot ζ n) (hn : n 0) :
theorem IsPrimitiveRoot.arg_ext {n : } {m : } {ζ : } {μ : } (hζ : IsPrimitiveRoot ζ n) (hμ : IsPrimitiveRoot μ m) (hn : n 0) (hm : m 0) (h : Complex.arg ζ = Complex.arg μ) :
ζ = μ
theorem IsPrimitiveRoot.arg_eq_zero_iff {n : } {ζ : } (hζ : IsPrimitiveRoot ζ n) (hn : n 0) :
Complex.arg ζ = 0 ζ = 1
theorem IsPrimitiveRoot.arg_eq_pi_iff {n : } {ζ : } (hζ : IsPrimitiveRoot ζ n) (hn : n 0) :
theorem IsPrimitiveRoot.arg {n : } {ζ : } (h : IsPrimitiveRoot ζ n) (hn : n 0) :
i, Complex.arg ζ = i / n * (2 * Real.pi) IsCoprime i n Int.natAbs i < n