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 : Nat) (h0 : Ne n 0) (hi : i.Coprime n) : IsPrimitiveRoot (exp (HMul.hMul (HMul.hMul (HMul.hMul 2 (ofReal Real.pi)) I) (HDiv.hDiv i.cast n.cast))) n

theorem Complex.isPrimitiveRoot_exp (n : Nat) (h0 : Ne n 0) : IsPrimitiveRoot (exp (HDiv.hDiv (HMul.hMul (HMul.hMul 2 (ofReal Real.pi)) I) n.cast)) n

theorem Complex.isPrimitiveRoot_iff (ζ : Complex) (n : Nat) (hn : Ne n 0) : Iff (IsPrimitiveRoot ζ n) (Exists fun (i : Nat) => And (LT.lt i n) (Exists fun (x : i.Coprime n) => Eq (exp (HMul.hMul (HMul.hMul (HMul.hMul 2 (ofReal Real.pi)) I) (HDiv.hDiv i.cast n.cast))) ζ))

theorem Complex.mem_rootsOfUnity (n : Nat) [NeZero n] (x : Units Complex) : Iff (Membership.mem (rootsOfUnity n Complex) x) (Exists fun (i : Nat) => And (LT.lt i n) (Eq (exp (HMul.hMul (HMul.hMul (HMul.hMul 2 (ofReal Real.pi)) I) (HDiv.hDiv i.cast n.cast))) x.val))

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 : Nat) [NeZero n] : Eq (Fintype.card (Subtype fun (x : Units Complex) => Membership.mem (rootsOfUnity n Complex) x)) n

theorem Complex.card_primitiveRoots (k : Nat) : Eq (primitiveRoots k Complex).card k.totient

theorem IsPrimitiveRoot.norm'_eq_one {ζ : Complex} {n : Nat} (h : IsPrimitiveRoot ζ n) (hn : Ne n 0) : Eq (Norm.norm ζ) 1

theorem IsPrimitiveRoot.nnnorm_eq_one {ζ : Complex} {n : Nat} (h : IsPrimitiveRoot ζ n) (hn : Ne n 0) : Eq (NNNorm.nnnorm ζ) 1

theorem IsPrimitiveRoot.arg_ext {n m : Nat} {ζ μ : Complex} (hζ : IsPrimitiveRoot ζ n) (hμ : IsPrimitiveRoot μ m) (hn : Ne n 0) (hm : Ne m 0) (h : Eq ζ.arg μ.arg) : Eq ζ μ

theorem IsPrimitiveRoot.arg_eq_zero_iff {n : Nat} {ζ : Complex} (hζ : IsPrimitiveRoot ζ n) (hn : Ne n 0) : Iff (Eq ζ.arg 0) (Eq ζ 1)

theorem IsPrimitiveRoot.arg_eq_pi_iff {n : Nat} {ζ : Complex} (hζ : IsPrimitiveRoot ζ n) (hn : Ne n 0) : Iff (Eq ζ.arg Real.pi) (Eq ζ (-1))

theorem IsPrimitiveRoot.arg {n : Nat} {ζ : Complex} (h : IsPrimitiveRoot ζ n) (hn : Ne n 0) : Exists fun (i : Int) => And (Eq ζ.arg (HMul.hMul (HDiv.hDiv i.cast n.cast) (HMul.hMul 2 Real.pi))) (And (IsCoprime i n.cast) (LT.lt i.natAbs n))

theorem Complex.norm_eq_one_of_mem_rootsOfUnity {ζ : Units Complex} {n : Nat} [NeZero n] (hζ : Membership.mem (rootsOfUnity n Complex) ζ) : Eq (Norm.norm ζ.val) 1