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 : i.Coprime n) :
theorem Complex.isPrimitiveRoot_iff (ζ : ) (n : ) (hn : n 0) :
IsPrimitiveRoot ζ n i < n, ∃ (_ : i.Coprime n), Complex.exp (2 * Real.pi * Complex.I * (i / n)) = ζ
theorem Complex.mem_rootsOfUnity (n : ℕ+) (x : ˣ) :
x rootsOfUnity n 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 Complex.card_primitiveRoots (k : ) :
(primitiveRoots k ).card = k.totient
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 : ζ.arg = μ.arg) :
ζ = μ
theorem IsPrimitiveRoot.arg_eq_zero_iff {n : } {ζ : } (hζ : IsPrimitiveRoot ζ n) (hn : n 0) :
ζ.arg = 0 ζ = 1
theorem IsPrimitiveRoot.arg_eq_pi_iff {n : } {ζ : } (hζ : IsPrimitiveRoot ζ n) (hn : n 0) :
ζ.arg = Real.pi ζ = -1
theorem IsPrimitiveRoot.arg {n : } {ζ : } (h : IsPrimitiveRoot ζ n) (hn : n 0) :
∃ (i : ), ζ.arg = i / n * (2 * Real.pi) IsCoprime i n i.natAbs < n