n : ℕ+
x : ℂˣ
⊢ ↑x ^ ↑n = 1 ↔ ∃ i, i < ↑n ∧ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
n : ℕ+
x : ℂˣ
⊢ x ∈ rootsOfUnity n ℂ ↔ ∃ i, i < ↑n ∧ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
rw [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one]
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
⊢ ↑x ^ ↑n = 1 ↔ ∃ i, i < ↑n ∧ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
n : ℕ+
x : ℂˣ
⊢ ↑x ^ ↑n = 1 ↔ ∃ i, i < ↑n ∧ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
have hn0 : (n : ℂ) ≠ 0 := by exact_mod_cast n.ne_zero
case mp
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
⊢ ↑x ^ ↑n = 1 → ∃ i, i < ↑n ∧ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x

case mpr
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
⊢ (∃ i, i < ↑n ∧ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x) → ↑x ^ ↑n = 1
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
⊢ ↑x ^ ↑n = 1 ↔ ∃ i, i < ↑n ∧ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
constructor
no goals
n : ℕ+
x : ℂˣ
⊢ ↑↑n ≠ 0
exact_mod_cast n.ne_zero
case mp
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
h : ↑x ^ ↑n = 1
⊢ ∃ i, i < ↑n ∧ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
case mp
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
⊢ ↑x ^ ↑n = 1 → ∃ i, i < ↑n ∧ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
intro h
case mp.intro.intro
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
h : ↑x ^ ↑n = 1
i : ℕ
hi : i < ↑n
H : exp (2 * ↑π * I / ↑↑n) ^ i = ↑x
⊢ ∃ i, i < ↑n ∧ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
case mp
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
h : ↑x ^ ↑n = 1
⊢ ∃ i, i < ↑n ∧ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
obtain ⟨i, hi, H⟩ : ∃ i < (n : ℕ), exp (2 * π * I / n) ^ i = x := by
  simpa only using (isPrimitiveRoot_exp n n.ne_zero).eq_pow_of_pow_eq_one h n.pos
case mp.intro.intro
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
h : ↑x ^ ↑n = 1
i : ℕ
hi : i < ↑n
H : exp (2 * ↑π * I / ↑↑n) ^ i = ↑x
⊢ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
case mp.intro.intro
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
h : ↑x ^ ↑n = 1
i : ℕ
hi : i < ↑n
H : exp (2 * ↑π * I / ↑↑n) ^ i = ↑x
⊢ ∃ i, i < ↑n ∧ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
refine' ⟨i, hi, _⟩
case mp.intro.intro
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
h : ↑x ^ ↑n = 1
i : ℕ
hi : i < ↑n
H : exp (2 * ↑π * I / ↑↑n) ^ i = ↑x
⊢ exp (2 * ↑π * I * (↑i / ↑↑n)) = exp (↑i * (2 * ↑π * I / ↑↑n))
case mp.intro.intro
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
h : ↑x ^ ↑n = 1
i : ℕ
hi : i < ↑n
H : exp (2 * ↑π * I / ↑↑n) ^ i = ↑x
⊢ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
rw [← H, ← exp_nat_mul]
case mp.intro.intro.e_z
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
h : ↑x ^ ↑n = 1
i : ℕ
hi : i < ↑n
H : exp (2 * ↑π * I / ↑↑n) ^ i = ↑x
⊢ 2 * ↑π * I * (↑i / ↑↑n) = ↑i * (2 * ↑π * I / ↑↑n)
case mp.intro.intro
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
h : ↑x ^ ↑n = 1
i : ℕ
hi : i < ↑n
H : exp (2 * ↑π * I / ↑↑n) ^ i = ↑x
⊢ exp (2 * ↑π * I * (↑i / ↑↑n)) = exp (↑i * (2 * ↑π * I / ↑↑n))
congr 1
no goals
case mp.intro.intro.e_z
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
h : ↑x ^ ↑n = 1
i : ℕ
hi : i < ↑n
H : exp (2 * ↑π * I / ↑↑n) ^ i = ↑x
⊢ 2 * ↑π * I * (↑i / ↑↑n) = ↑i * (2 * ↑π * I / ↑↑n)
field_simp [hn0, mul_comm (i : ℂ)]
no goals
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
h : ↑x ^ ↑n = 1
⊢ ∃ i, i < ↑n ∧ exp (2 * ↑π * I / ↑↑n) ^ i = ↑x
simpa only using (isPrimitiveRoot_exp n n.ne_zero).eq_pow_of_pow_eq_one h n.pos
case mpr.intro.intro
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
i : ℕ
left✝ : i < ↑n
H : exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
⊢ ↑x ^ ↑n = 1
case mpr
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
⊢ (∃ i, i < ↑n ∧ exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x) → ↑x ^ ↑n = 1
rintro ⟨i, _, H⟩
case mpr.intro.intro
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
i : ℕ
left✝ : i < ↑n
H : exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
⊢ ∃ n_1, ↑↑n * (2 * ↑π * I * (↑i / ↑↑n)) = ↑n_1 * (2 * ↑π * I)
case mpr.intro.intro
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
i : ℕ
left✝ : i < ↑n
H : exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
⊢ ↑x ^ ↑n = 1
rw [← H, ← exp_nat_mul, exp_eq_one_iff]
case mpr.intro.intro
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
i : ℕ
left✝ : i < ↑n
H : exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
⊢ ↑↑n * (2 * ↑π * I * (↑i / ↑↑n)) = ↑↑i * (2 * ↑π * I)
case mpr.intro.intro
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
i : ℕ
left✝ : i < ↑n
H : exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
⊢ ∃ n_1, ↑↑n * (2 * ↑π * I * (↑i / ↑↑n)) = ↑n_1 * (2 * ↑π * I)
use i
no goals
case mpr.intro.intro
n : ℕ+
x : ℂˣ
hn0 : ↑↑n ≠ 0
i : ℕ
left✝ : i < ↑n
H : exp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
⊢ ↑↑n * (2 * ↑π * I * (↑i / ↑↑n)) = ↑↑i * (2 * ↑π * I)
field_simp [hn0, mul_comm ((n : ℕ) : ℂ), mul_comm (i : ℂ)]