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 (2 * ↑Real.pi * Complex.I * (↑i / ↑n))) n

theorem Complex.isPrimitiveRoot_exp (n : ℕ) (h0 : n ≠ 0) : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) 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 : ℕ) [NeZero 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_rootsOfUnity (n : ℕ) [NeZero n] : Fintype.card ↥(rootsOfUnity n ℂ) = 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) : ‖ζ‖₊ = 1

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

theorem Complex.norm_eq_one_of_mem_rootsOfUnity {ζ : ℂˣ} {n : ℕ} [NeZero n] (hζ : ζ ∈ rootsOfUnity n ℂ) : ‖↑ζ‖ = 1