Complex roots of unity #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 complex n-th roots of unity are exactly the complex numbers of the form e ^ (2 * real.pi * complex.I * (i / n)) for some i < n.
complex.card_roots_of_unity: the number of n-th roots of unity is exactly n.

source

theorem complex.is_primitive_root_exp_of_coprime (i n : ℕ) (h0 : n ≠ 0) (hi : i.coprime n) :

is_primitive_root (cexp (2 * ↑real.pi * complex.I * (↑i / ↑n))) n

source

theorem complex.is_primitive_root_exp (n : ℕ) (h0 : n ≠ 0) :

is_primitive_root (cexp (2 * ↑real.pi * complex.I / ↑n)) n

source

theorem complex.is_primitive_root_iff (ζ : ℂ) (n : ℕ) (hn : n ≠ 0) :

is_primitive_root ζ n ↔ ∃ (i : ℕ) (H : i < n) (hi : i.coprime n), cexp (2 * ↑real.pi * complex.I * (↑i / ↑n)) = ζ

source

theorem complex.mem_roots_of_unity (n : ℕ+) (x : ℂ ˣ) :

x ∈ roots_of_unity n ℂ ↔ ∃ (i : ℕ) (H : i < ↑n), cexp (2 * ↑real.pi * complex.I * (↑i / ↑n)) = ↑x

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

source

theorem complex.card_roots_of_unity (n : ℕ+) :

fintype.card ↥(roots_of_unity n ℂ) = ↑n

source

theorem complex.card_primitive_roots (k : ℕ) :

(primitive_roots k ℂ).card = k.totient

source

theorem is_primitive_root.norm'_eq_one {ζ : ℂ} {n : ℕ} (h : is_primitive_root ζ n) (hn : n ≠ 0) :

‖ζ‖ = 1

source

theorem is_primitive_root.nnnorm_eq_one {ζ : ℂ} {n : ℕ} (h : is_primitive_root ζ n) (hn : n ≠ 0) :

‖ζ‖₊ = 1

source

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) :

ζ = μ

source

theorem is_primitive_root.arg_eq_zero_iff {n : ℕ} {ζ : ℂ} (hζ : is_primitive_root ζ n) (hn : n ≠ 0) :

ζ.arg = 0 ↔ ζ = 1

source

theorem is_primitive_root.arg_eq_pi_iff {n : ℕ} {ζ : ℂ} (hζ : is_primitive_root ζ n) (hn : n ≠ 0) :

ζ.arg = real.pi ↔ ζ = -1

source

theorem is_primitive_root.arg {n : ℕ} {ζ : ℂ} (h : is_primitive_root ζ n) (hn : n ≠ 0) :

∃ (i : ℤ), ζ.arg = ↑i / ↑n * (2 * real.pi) ∧ is_coprime i ↑n ∧ i.nat_abs < n