2. Roots of unity
This section defines roots of unity and proves various basic facts about them.
Throughout this section we assume that d ≥ 1.
Lean code
variable (d : ℕ) [NeZero d]
Lemma2.2
Group: Roots of unity and their basic properties. (10)
- Definition 2.3
- Lemma 2.4
- Lemma 2.5
- Lemma 2.7
- Definition 2.10
- Lemma 2.11
- Lemma 2.12
- Lemma 2.13
- Lemma 2.14
- Lemma 2.16
Preview
Definition 2.3
Associated Lean declarations
-
d_invertible[complete]
d is invertible in ℂ.
Proof
The inverse of d exists since d ∈ ℕ and d ≠ 0.
Lean code for Lemma2.2
Associated Lean declarations
-
d_invertible[complete]
Associated Lean declarations
-
d_invertible[complete]
lemma d_invertible : IsUnit (d : ℂ) := d:ℕinst✝:NeZero d⊢ IsUnit ↑d
d:ℕinst✝:NeZero d⊢ ¬d = 0
All goals completed! 🐙
Define the primitive d-th root of unity.
Definition2.3
Group: Roots of unity and their basic properties. (10)
- Lemma 2.2
- Lemma 2.4
- Lemma 2.5
- Lemma 2.7
- Definition 2.10
- Lemma 2.11
- Lemma 2.12
- Lemma 2.13
- Lemma 2.14
- Lemma 2.16
Preview
Lemma 2.2
Associated Lean declarations
-
ω[complete]
Used by 3
Preview
Definition 4.32
Let ω = \exp(2πi/d) be the primitive d-th root of unity.
Lean code for Definition2.3
Associated Lean declarations
-
ω[complete]
Associated Lean declarations
-
ω[complete]
noncomputable
def ω : ℂ :=
Complex.exp (2 * Real.pi * Complex.I / d)
Lemma2.4
Group: Roots of unity and their basic properties. (10)
- Lemma 2.2
- Definition 2.3
- Lemma 2.5
- Lemma 2.7
- Definition 2.10
- Lemma 2.11
- Lemma 2.12
- Lemma 2.13
- Lemma 2.14
- Lemma 2.16
Preview
Lemma 2.2
Associated Lean declarations
-
omega_ne_zero[complete]
ω ≠ 0.
Lean code for Lemma2.4
Associated Lean declarations
-
omega_ne_zero[complete]
Associated Lean declarations
-
omega_ne_zero[complete]
omit [NeZero d] in
lemma omega_ne_zero : ω d ≠ 0 := d:ℕ⊢ ω d ≠ 0
All goals completed! 🐙
Lemma2.5
Group: Roots of unity and their basic properties. (10)
- Lemma 2.2
- Definition 2.3
- Lemma 2.4
- Lemma 2.7
- Definition 2.10
- Lemma 2.11
- Lemma 2.12
- Lemma 2.13
- Lemma 2.14
- Lemma 2.16
Preview
Lemma 2.2
Associated Lean declarations
-
omega_pow_d_eq_one[complete]
ω^d = 1.
Proof
ω^d = (\exp(2πi/d))^d = \exp(d(2πi/d)) = \exp(2πi) = 1 where we could cancel d since d ≠ 0.
Lean code for Lemma2.5
Associated Lean declarations
-
omega_pow_d_eq_one[complete]
Associated Lean declarations
-
omega_pow_d_eq_one[complete]
lemma omega_pow_d_eq_one : (ω d)^d = 1 := d:ℕinst✝:NeZero d⊢ ω d ^ d = 1
d:ℕinst✝:NeZero d⊢ Complex.exp (2 * ↑Real.pi * Complex.I / ↑d) ^ d = 1
d:ℕinst✝:NeZero d⊢ Complex.exp (↑d * (2 * ↑Real.pi * Complex.I / ↑d)) = 1
d:ℕinst✝:NeZero d⊢ Complex.exp (2 * ↑Real.pi * Complex.I) = 1d:ℕinst✝:NeZero d⊢ IsUnit ↑d
d:ℕinst✝:NeZero d⊢ Complex.exp (2 * ↑Real.pi * Complex.I) = 1 All goals completed! 🐙
d:ℕinst✝:NeZero d⊢ IsUnit ↑d All goals completed! 🐙
Lean code
Associated Lean declarations
-
order_omega[complete]
Associated Lean declarations
-
order_omega[complete]
lemma order_omega : orderOf (ω d) = d := d:ℕinst✝:NeZero d⊢ orderOf (ω d) = d
d:ℕinst✝:NeZero d⊢ 0 < dd:ℕinst✝:NeZero d⊢ ω d ^ d = 1d:ℕinst✝:NeZero d⊢ ∀ (p : ℕ), Nat.Prime p → p ∣ d → ω d ^ (d / p) ≠ 1
d:ℕinst✝:NeZero d⊢ ω d ^ d = 1d:ℕinst✝:NeZero d⊢ ∀ (p : ℕ), Nat.Prime p → p ∣ d → ω d ^ (d / p) ≠ 1
d:ℕinst✝:NeZero d⊢ ∀ (p : ℕ), Nat.Prime p → p ∣ d → ω d ^ (d / p) ≠ 1
intro p d:ℕinst✝:NeZero dp:ℕhp:Nat.Prime p⊢ p ∣ d → ω d ^ (d / p) ≠ 1 d:ℕinst✝:NeZero dp:ℕhp:Nat.Prime phpdivd:p ∣ d⊢ ω d ^ (d / p) ≠ 1
d:ℕinst✝:NeZero dp:ℕhp:Nat.Prime phpdivd:p ∣ d⊢ Complex.exp (2 * ↑Real.pi * Complex.I / ↑d) ^ (d / p) ≠ 1
d:ℕinst✝:NeZero dp:ℕhp:Nat.Prime phpdivd:p ∣ d⊢ Complex.exp (↑(d / p) * (2 * ↑Real.pi * Complex.I / ↑d)) ≠ 1
d:ℕinst✝:NeZero dp:ℕhp:Nat.Prime phpdivd:p ∣ d⊢ Complex.exp (↑d / ↑p * (2 * ↑Real.pi * Complex.I / ↑d)) ≠ 1
d:ℕinst✝:NeZero dp:ℕhp:Nat.Prime phpdivd:p ∣ d⊢ Complex.exp (↑d * (2 * ↑Real.pi * Complex.I) / (↑p * ↑d)) ≠ 1
nth_rw 4 [mul_commd:ℕinst✝:NeZero dp:ℕhp:Nat.Prime phpdivd:p ∣ d⊢ Complex.exp (↑d * (2 * ↑Real.pi * Complex.I) / (↑d * ↑p)) ≠ 1
d:ℕinst✝:NeZero dp:ℕhp:Nat.Prime phpdivd:p ∣ d⊢ Complex.exp (↑d / ↑d * (2 * ↑Real.pi * Complex.I / ↑p)) ≠ 1
--#check div_self (Nat.cast_ne_zero.2 (NeZero.ne d))
--rw [div_self, one_mul]
d:ℕinst✝:NeZero dp:ℕhp:Nat.Prime phpdivd:p ∣ d⊢ Complex.exp (↑(d / d) * (2 * ↑Real.pi * Complex.I / ↑p)) ≠ 1
d:ℕinst✝:NeZero dp:ℕhp:Nat.Prime phpdivd:p ∣ d⊢ ¬Complex.exp (2 * ↑Real.pi * Complex.I / ↑p) = 1
d:ℕinst✝:NeZero dp:ℕhp:Nat.Prime phpdivd:p ∣ d⊢ ¬Complex.exp (2 * ↑Real.pi * Complex.I * 1 / ↑p) = 1
nth_rw 1 [← (Nat.cast_one (R:= ℂ )) d:ℕinst✝:NeZero dp:ℕhp:Nat.Prime phpdivd:p ∣ d⊢ ¬Complex.exp (2 * ↑Real.pi * Complex.I * ↑1 / ↑p) = 1
d:ℕinst✝:NeZero dp:ℕhp:Nat.Prime phpdivd:p ∣ dhfalse:Complex.exp (2 * ↑Real.pi * Complex.I * ↑1 / ↑p) = 1⊢ False
All goals completed! 🐙
This is an additional corrolary that is nice to have.
Lemma2.7
Group: Roots of unity and their basic properties. (10)
- Lemma 2.2
- Definition 2.3
- Lemma 2.4
- Lemma 2.5
- Definition 2.10
- Lemma 2.11
- Lemma 2.12
- Lemma 2.13
- Lemma 2.14
- Lemma 2.16
Preview
Lemma 2.2
Associated Lean declarations
-
omega_pow_n_mod_d[complete]
ω^n = ω^{n \% d}.
Lean code for Lemma2.7
Associated Lean declarations
-
omega_pow_n_mod_d[complete]
Associated Lean declarations
-
omega_pow_n_mod_d[complete]
lemma omega_pow_n_mod_d :
∀ n : Nat, (ω d) ^ n = (ω d) ^ (n % d) := d:ℕinst✝:NeZero d⊢ ∀ (n : ℕ), ω d ^ n = ω d ^ (n % d)
d:ℕinst✝:NeZero dn:ℕ⊢ ω d ^ n = ω d ^ (n % d)
nth_rw 1 [←(Nat.mod_add_div n d)d:ℕinst✝:NeZero dn:ℕ⊢ ω d ^ (n % d + d * (n / d)) = ω d ^ (n % d)
All goals completed! 🐙
Lean code
Associated Lean declarations
-
omega_pow_k_mod_d_eq_pow_k_int[complete]
Associated Lean declarations
-
omega_pow_k_mod_d_eq_pow_k_int[complete]
lemma omega_pow_k_mod_d_eq_pow_k_int :
∀ k : Int, (ω d) ^ k = (ω d) ^ (k % d) := d:ℕinst✝:NeZero d⊢ ∀ (k : ℤ), ω d ^ k = ω d ^ (k % ↑d)
d:ℕinst✝:NeZero dk:ℤ⊢ ω d ^ k = ω d ^ (k % ↑d)
nth_rw 1 [← (Int.emod_add_ediv_mul k d)d:ℕinst✝:NeZero dk:ℤ⊢ ω d ^ (k % ↑d + k / ↑d * ↑d) = ω d ^ (k % ↑d)
d:ℕinst✝:NeZero dk:ℤ⊢ ω d ^ (k % ↑d) * ω d ^ (k / ↑d * ↑d) = ω d ^ (k % ↑d)d:ℕinst✝:NeZero dk:ℤ⊢ ω d ≠ 0 ∨ k % ↑d + k / ↑d * ↑d ≠ 0 ∨ k % ↑d = 0 ∧ k / ↑d * ↑d = 0
nth_rw 2 [mul_commd:ℕinst✝:NeZero dk:ℤ⊢ ω d ^ (k % ↑d) * ω d ^ (↑d * (k / ↑d)) = ω d ^ (k % ↑d)d:ℕinst✝:NeZero dk:ℤ⊢ ω d ≠ 0 ∨ k % ↑d + k / ↑d * ↑d ≠ 0 ∨ k % ↑d = 0 ∧ k / ↑d * ↑d = 0
d:ℕinst✝:NeZero dk:ℤ⊢ ω d ^ (k % ↑d) * (ω d ^ ↑d) ^ (k / ↑d) = ω d ^ (k % ↑d)d:ℕinst✝:NeZero dk:ℤ⊢ ω d ≠ 0 ∨ k % ↑d + k / ↑d * ↑d ≠ 0 ∨ k % ↑d = 0 ∧ k / ↑d * ↑d = 0
d:ℕinst✝:NeZero dk:ℤ⊢ ω d ^ (k % ↑d) * (ω d ^ d) ^ (k / ↑d) = ω d ^ (k % ↑d)d:ℕinst✝:NeZero dk:ℤ⊢ ω d ≠ 0 ∨ k % ↑d + k / ↑d * ↑d ≠ 0 ∨ k % ↑d = 0 ∧ k / ↑d * ↑d = 0
d:ℕinst✝:NeZero dk:ℤ⊢ ω d ≠ 0 ∨ k % ↑d + k / ↑d * ↑d ≠ 0 ∨ k % ↑d = 0 ∧ k / ↑d * ↑d = 0
d:ℕinst✝:NeZero dk:ℤ⊢ ω d ≠ 0
d:ℕinst✝:NeZero dk:ℤ⊢ Complex.exp (2 * ↑Real.pi * Complex.I / ↑d) ≠ 0
All goals completed! 🐙
Lean code
Associated Lean declarations
-
omega_pow_k_mod_d_eq_pow_k_zmod[complete]
Associated Lean declarations
-
omega_pow_k_mod_d_eq_pow_k_zmod[complete]
lemma omega_pow_k_mod_d_eq_pow_k_zmod :
∀ k : Int, (ω d) ^ k = (ω d) ^ (k : ZMod d).val := d:ℕinst✝:NeZero d⊢ ∀ (k : ℤ), ω d ^ k = ω d ^ (↑k).val
d:ℕinst✝:NeZero dk:ℤ⊢ ω d ^ k = ω d ^ (↑k).val
d:ℕinst✝:NeZero dk:ℤ⊢ ω d ^ (k % ↑d) = ω d ^ (↑k).val
d:ℕinst✝:NeZero dk:ℤ⊢ ω d ^ ↑(↑k).val = ω d ^ (↑k).val
All goals completed! 🐙
We will also need another root of unity which we call τ.
Definition2.10
Group: Roots of unity and their basic properties. (10)
- Lemma 2.2
- Definition 2.3
- Lemma 2.4
- Lemma 2.5
- Lemma 2.7
- Lemma 2.11
- Lemma 2.12
- Lemma 2.13
- Lemma 2.14
- Lemma 2.16
Preview
Lemma 2.2
Associated Lean declarations
-
τ[complete]
Used by 3
Preview
Definition 5.46
Let τ = -\exp(πi/d).
Lean code for Definition2.10
Associated Lean declarations
-
τ[complete]
Associated Lean declarations
-
τ[complete]
noncomputable
def τ : ℂ :=
- Complex.exp (Real.pi * Complex.I / d)
Lemma2.11
Group: Roots of unity and their basic properties. (10)
- Lemma 2.2
- Definition 2.3
- Lemma 2.4
- Lemma 2.5
- Lemma 2.7
- Definition 2.10
- Lemma 2.12
- Lemma 2.13
- Lemma 2.14
- Lemma 2.16
Preview
Lemma 2.2
Associated Lean declarations
-
tau_sq_eq_omega[sorry in proof]
Used by 3
Preview
Theorem 7.1
τ^2 = ω.
Proof
τ^2 = (-\exp(πi/d))^2 = (-1)^2 · (\exp(πi/d))^2 = 1 · \exp(2πi/d) = ω.
Lean code for Lemma2.11
Associated Lean declarations
-
tau_sq_eq_omega[sorry in proof]
Associated Lean declarations
-
tau_sq_eq_omega[sorry in proof]
lemma tau_sq_eq_omega : (τ d)^2 = ω d := d:ℕinst✝:NeZero d⊢ τ d ^ 2 = ω d
All goals completed! 🐙
Lemma2.12
Group: Roots of unity and their basic properties. (10)
- Lemma 2.2
- Definition 2.3
- Lemma 2.4
- Lemma 2.5
- Lemma 2.7
- Definition 2.10
- Lemma 2.11
- Lemma 2.13
- Lemma 2.14
- Lemma 2.16
Preview
Lemma 2.2
Associated Lean declarations
-
tau_pow_d_eq_one_of_odd[complete]
If d is odd then τ^d = 1.
Proof
τ^d = (-\exp(πi/d))^d = (-1)^d · (\exp(πi/d))^d = (-1)^d · \exp(πi) = (-1)^d · (-1) = (-1)^{d+1} = 1 when d is odd.
Lean code for Lemma2.12
Associated Lean declarations
-
tau_pow_d_eq_one_of_odd[complete]
Associated Lean declarations
-
tau_pow_d_eq_one_of_odd[complete]
lemma tau_pow_d_eq_one_of_odd (hodd : Odd d) :
(τ d)^d = 1 := d:ℕinst✝:NeZero dhodd:Odd d⊢ τ d ^ d = 1
calc
(-Complex.exp (↑Real.pi * Complex.I * (↑d)⁻¹)) ^ d
= (-1 : ℂ)^d *
Complex.exp (↑Real.pi *
Complex.I * (↑d)⁻¹) ^ d := d:ℕinst✝:NeZero dhodd:Odd d⊢ (-Complex.exp (↑Real.pi * Complex.I * (↑d)⁻¹)) ^ d = (-1) ^ d * Complex.exp (↑Real.pi * Complex.I * (↑d)⁻¹) ^ d
All goals completed! 🐙
_ = (-1 : ℂ)^d *
Complex.exp (↑Real.pi *
Complex.I * ↑d * (↑d)⁻¹) := d:ℕinst✝:NeZero dhodd:Odd d⊢ (-1) ^ d * Complex.exp (↑Real.pi * Complex.I * (↑d)⁻¹) ^ d = (-1) ^ d * Complex.exp (↑Real.pi * Complex.I * ↑d * (↑d)⁻¹)
All goals completed! 🐙
_ = (-1 : ℂ)^d *
Complex.exp (↑Real.pi * Complex.I) := d:ℕinst✝:NeZero dhodd:Odd d⊢ (-1) ^ d * Complex.exp (↑Real.pi * Complex.I * ↑d * (↑d)⁻¹) = (-1) ^ d * Complex.exp (↑Real.pi * Complex.I)
All goals completed! 🐙
_ = (-1)^(d+1) := d:ℕinst✝:NeZero dhodd:Odd d⊢ (-1) ^ d * Complex.exp (↑Real.pi * Complex.I) = (-1) ^ (d + 1)
All goals completed! 🐙
_ = 1 := d:ℕinst✝:NeZero dhodd:Odd d⊢ (-1) ^ (d + 1) = 1
d:ℕinst✝:NeZero dhodd:Odd d⊢ Even (d + 1)d:ℕinst✝:NeZero dhodd:Odd d⊢ -1 ≠ 1
d:ℕinst✝:NeZero dhodd:Odd d⊢ Even (d + 1) d:ℕinst✝:NeZero dk:ℕhk:d = 2 * k + 1⊢ Even (d + 1)
d:ℕinst✝:NeZero dk:ℕhk:d = 2 * k + 1⊢ ∃ r, d + 1 = r + r
d:ℕinst✝:NeZero dk:ℕhk:d = 2 * k + 1⊢ d + 1 = k + 1 + (k + 1)
All goals completed! 🐙
d:ℕinst✝:NeZero dhodd:Odd d⊢ -1 ≠ 1 All goals completed! 🐙
Lemma2.13
Group: Roots of unity and their basic properties. (10)
- Lemma 2.2
- Definition 2.3
- Lemma 2.4
- Lemma 2.5
- Lemma 2.7
- Definition 2.10
- Lemma 2.11
- Lemma 2.12
- Lemma 2.14
- Lemma 2.16
Preview
Lemma 2.2
Associated Lean declarations
-
tau_pow_d2_one[complete]
τ^{d^2} = 1.
Proof
τ^{d^2} = (-\exp(πi/d))^{d^2} = (-1)^{d^2} · (-1)^d = (-1)^{d(d+1)} = 1
since either d or d+1 is even.
Lean code for Lemma2.13
Associated Lean declarations
-
tau_pow_d2_one[complete]
Associated Lean declarations
-
tau_pow_d2_one[complete]
lemma tau_pow_d2_one : (τ d) ^ (d ^ 2) = 1 := d:ℕinst✝:NeZero d⊢ τ d ^ d ^ 2 = 1
d:ℕinst✝:NeZero d⊢ (-Complex.exp (↑Real.pi * Complex.I / ↑d)) ^ d ^ 2 = 1
d:ℕinst✝:NeZero d⊢ (-1 * Complex.exp (↑Real.pi * Complex.I / ↑d)) ^ d ^ 2 = 1
d:ℕinst✝:NeZero d⊢ (-1 * Complex.exp (↑Real.pi * Complex.I / ↑d)) ^ (d * d) = 1
d:ℕinst✝:NeZero d⊢ (-1) ^ (d * d) * Complex.exp (↑Real.pi * Complex.I / ↑d) ^ (d * d) = 1
d:ℕinst✝:NeZero d⊢ (-1) ^ (d * d) * Complex.exp (↑(d * d) * (↑Real.pi * Complex.I / ↑d)) = 1
d:ℕinst✝:NeZero d⊢ (-1) ^ (d * d) * Complex.exp (↑d * ↑d * (↑Real.pi * Complex.I / ↑d)) = 1
d:ℕinst✝:NeZero d⊢ (-1) ^ (d * d) * Complex.exp (↑d * (↑d * (↑Real.pi * Complex.I / ↑d))) = 1
d:ℕinst✝:NeZero d⊢ (-1) ^ (d * d) * Complex.exp (↑d * (↑Real.pi * Complex.I)) = 1d:ℕinst✝:NeZero d⊢ IsUnit ↑d
d:ℕinst✝:NeZero d⊢ (-1) ^ (d * d) * Complex.exp (↑Real.pi * Complex.I) ^ d = 1d:ℕinst✝:NeZero d⊢ IsUnit ↑d
d:ℕinst✝:NeZero d⊢ (-1) ^ (d * d) * (-1) ^ d = 1d:ℕinst✝:NeZero d⊢ IsUnit ↑d
d:ℕinst✝:NeZero d⊢ (-1) ^ (d * d + d) = 1d:ℕinst✝:NeZero d⊢ IsUnit ↑d
d:ℕinst✝:NeZero d⊢ (-1) ^ (d * (d + 1)) = 1d:ℕinst✝:NeZero d⊢ IsUnit ↑d
d:ℕinst✝:NeZero d⊢ Even (d * (d + 1))d:ℕinst✝:NeZero d⊢ -1 ≠ 1d:ℕinst✝:NeZero d⊢ IsUnit ↑d
d:ℕinst✝:NeZero d⊢ -1 ≠ 1d:ℕinst✝:NeZero d⊢ IsUnit ↑d
d:ℕinst✝:NeZero d⊢ -1 ≠ 1 All goals completed! 🐙
d:ℕinst✝:NeZero d⊢ IsUnit ↑d All goals completed! 🐙
Lemma2.14
Group: Roots of unity and their basic properties. (10)
- Lemma 2.2
- Definition 2.3
- Lemma 2.4
- Lemma 2.5
- Lemma 2.7
- Definition 2.10
- Lemma 2.11
- Lemma 2.12
- Lemma 2.13
- Lemma 2.16
Preview
Lemma 2.2
Associated Lean declarations
-
tau_ne_zero[complete]
τ ≠ 0.
Lean code for Lemma2.14
Associated Lean declarations
-
tau_ne_zero[complete]
Associated Lean declarations
-
tau_ne_zero[complete]
omit [NeZero d] in
lemma tau_ne_zero : τ d ≠ 0 := d:ℕ⊢ τ d ≠ 0
d:ℕ⊢ -Complex.exp (↑Real.pi * Complex.I / ↑d) ≠ 0
d:ℕ⊢ - -Complex.exp (↑Real.pi * Complex.I / ↑d) ≠ 0
d:ℕ⊢ Complex.exp (↑Real.pi * Complex.I / ↑d) ≠ 0
All goals completed! 🐙
Lean code
Associated Lean declarations
-
mod_d_nonneg[complete]
Associated Lean declarations
-
mod_d_nonneg[complete]
lemma mod_d_nonneg (a : ℤ) : 0 ≤ a % ↑d := d:ℕinst✝:NeZero da:ℤ⊢ 0 ≤ a % ↑d
d:ℕinst✝:NeZero da:ℤ⊢ ↑d ≠ 0
All goals completed! 🐙
Lemma2.16
Group: Roots of unity and their basic properties. (10)
- Lemma 2.2
- Definition 2.3
- Lemma 2.4
- Lemma 2.5
- Lemma 2.7
- Definition 2.10
- Lemma 2.11
- Lemma 2.12
- Lemma 2.13
- Lemma 2.14
Preview
Lemma 2.2
Associated Lean declarations
-
tau_pow_n_mod_d_of_d_odd[complete]
If d is odd then τ^{n} = τ^{n \% d}.
Lean code for Lemma2.16
Associated Lean declarations
-
tau_pow_n_mod_d_of_d_odd[complete]
Associated Lean declarations
-
tau_pow_n_mod_d_of_d_odd[complete]
theorem tau_pow_n_mod_d_of_d_odd
(n d : ℕ) (hodd : Odd d) [NeZero d] :
τ d ^ n = τ d ^ (n % ↑d) :=
pow_eq_pow_mod n (tau_pow_d_eq_one_of_odd d hodd)
Lean code
Associated Lean declarations
-
tau_star[complete]
Associated Lean declarations
-
tau_star[complete]
theorem tau_star
(d : ℕ) (n : ℤ) [NeZero d] :
star (τ d ^ n) = τ d^(-n) := d:ℕn:ℤinst✝:NeZero d⊢ star (τ d ^ n) = τ d ^ (-n)
d:ℕn:ℤinst✝:NeZero d⊢ star ((-Complex.exp (↑Real.pi * Complex.I / ↑d)) ^ n) = (-Complex.exp (↑Real.pi * Complex.I / ↑d)) ^ (-n)
d:ℕn:ℤinst✝:NeZero d⊢ (-Complex.exp ((starRingEnd ℂ) (↑Real.pi * Complex.I / ↑d))) ^ n = (-Complex.exp (↑Real.pi * Complex.I / ↑d)) ^ (-n)
d:ℕn:ℤinst✝:NeZero d⊢ (-Complex.exp (-(↑Real.pi * Complex.I) / ↑d)) ^ n = (-Complex.exp (↑Real.pi * Complex.I / ↑d)) ^ (-n)
d:ℕn:ℤinst✝:NeZero dh:Even n⊢ (-Complex.exp (-(↑Real.pi * Complex.I) / ↑d)) ^ n = (-Complex.exp (↑Real.pi * Complex.I / ↑d)) ^ (-n)d:ℕn:ℤinst✝:NeZero dh:¬Even n⊢ (-Complex.exp (-(↑Real.pi * Complex.I) / ↑d)) ^ n = (-Complex.exp (↑Real.pi * Complex.I / ↑d)) ^ (-n)
d:ℕn:ℤinst✝:NeZero dh:Even n⊢ (-Complex.exp (-(↑Real.pi * Complex.I) / ↑d)) ^ n = (-Complex.exp (↑Real.pi * Complex.I / ↑d)) ^ (-n) d:ℕn:ℤinst✝:NeZero dh:Even n⊢ Complex.exp (-(↑Real.pi * Complex.I) / ↑d) ^ n = Complex.exp (↑Real.pi * Complex.I / ↑d) ^ (-n)
d:ℕn:ℤinst✝:NeZero dh:Even n⊢ Complex.exp (↑n * (-(↑Real.pi * Complex.I) / ↑d)) = Complex.exp (↑(-n) * (↑Real.pi * Complex.I / ↑d))
d:ℕn:ℤinst✝:NeZero dh:Even n⊢ Complex.exp (↑n * (-(↑Real.pi * Complex.I) / ↑d)) = Complex.exp (-↑n * (↑Real.pi * Complex.I / ↑d))
All goals completed! 🐙
d:ℕn:ℤinst✝:NeZero dh:Odd n⊢ (-Complex.exp (-(↑Real.pi * Complex.I) / ↑d)) ^ n = (-Complex.exp (↑Real.pi * Complex.I / ↑d)) ^ (-n)
d:ℕn:ℤinst✝:NeZero dh:Odd n⊢ -Complex.exp (-(↑Real.pi * Complex.I) / ↑d) ^ n = -Complex.exp (↑Real.pi * Complex.I / ↑d) ^ (-n)
d:ℕn:ℤinst✝:NeZero dh:Odd n⊢ -Complex.exp (↑n * (-(↑Real.pi * Complex.I) / ↑d)) = -Complex.exp (↑(-n) * (↑Real.pi * Complex.I / ↑d))
d:ℕn:ℤinst✝:NeZero dh:Odd n⊢ -Complex.exp (↑n * (-(↑Real.pi * Complex.I) / ↑d)) = -Complex.exp (-↑n * (↑Real.pi * Complex.I / ↑d))
All goals completed! 🐙