ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n ↔ ∃ i, i < n ∧ ∃ x, exp (2 * ↑π * I * (↑i / ↑n)) = ζ
ζ : ℂ
n : ℕ
hn : n ≠ 0
⊢ IsPrimitiveRoot ζ n ↔ ∃ i, i < n ∧ ∃ x, exp (2 * ↑π * I * (↑i / ↑n)) = ζ
have hn0 : (n : ℂ) ≠ 0 := by exact_mod_cast hn
case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n → ∃ i, i < n ∧ ∃ x, exp (2 * ↑π * I * (↑i / ↑n)) = ζ

case mpr
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (∃ i, i < n ∧ ∃ x, exp (2 * ↑π * I * (↑i / ↑n)) = ζ) → IsPrimitiveRoot ζ n
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n ↔ ∃ i, i < n ∧ ∃ x, exp (2 * ↑π * I * (↑i / ↑n)) = ζ
constructor
case mpr
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (∃ i, i < n ∧ ∃ x, exp (2 * ↑π * I * (↑i / ↑n)) = ζ) → IsPrimitiveRoot ζ n

case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n → ∃ i, i < n ∧ ∃ x, exp (2 * ↑π * I * (↑i / ↑n)) = ζ
case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n → ∃ i, i < n ∧ ∃ x, exp (2 * ↑π * I * (↑i / ↑n)) = ζ

case mpr
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (∃ i, i < n ∧ ∃ x, exp (2 * ↑π * I * (↑i / ↑n)) = ζ) → IsPrimitiveRoot ζ n
swap
case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
h : IsPrimitiveRoot ζ n
⊢ ∃ i, i < n ∧ ∃ x, exp (2 * ↑π * I * (↑i / ↑n)) = ζ
case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n → ∃ i, i < n ∧ ∃ x, exp (2 * ↑π * I * (↑i / ↑n)) = ζ
intro h
case mp.intro.intro
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
i : ℕ
hi : i < n
h : IsPrimitiveRoot (exp (2 * ↑π * I / ↑n) ^ i) n
⊢ ∃ i_1, i_1 < n ∧ ∃ x, exp (2 * ↑π * I * (↑i_1 / ↑n)) = exp (2 * ↑π * I / ↑n) ^ i
case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
h : IsPrimitiveRoot ζ n
⊢ ∃ i, i < n ∧ ∃ x, exp (2 * ↑π * I * (↑i / ↑n)) = ζ
obtain ⟨i, hi, rfl⟩ :=
  (isPrimitiveRoot_exp n hn).eq_pow_of_pow_eq_one h.pow_eq_one (Nat.pos_of_ne_zero hn)
case mp.intro.intro
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
i : ℕ
hi : i < n
h : IsPrimitiveRoot (exp (2 * ↑π * I / ↑n) ^ i) n
⊢ exp (2 * ↑π * I * (↑i / ↑n)) = exp (2 * ↑π * I / ↑n) ^ i
case mp.intro.intro
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
i : ℕ
hi : i < n
h : IsPrimitiveRoot (exp (2 * ↑π * I / ↑n) ^ i) n
⊢ ∃ i_1, i_1 < n ∧ ∃ x, exp (2 * ↑π * I * (↑i_1 / ↑n)) = exp (2 * ↑π * I / ↑n) ^ i
refine' ⟨i, hi, ((isPrimitiveRoot_exp n hn).pow_iff_coprime (Nat.pos_of_ne_zero hn) i).mp h, _⟩
case mp.intro.intro
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
i : ℕ
hi : i < n
h : IsPrimitiveRoot (exp (2 * ↑π * I / ↑n) ^ i) n
⊢ exp (2 * ↑π * I * (↑i / ↑n)) = exp (↑i * (2 * ↑π * I / ↑n))
case mp.intro.intro
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
i : ℕ
hi : i < n
h : IsPrimitiveRoot (exp (2 * ↑π * I / ↑n) ^ i) n
⊢ exp (2 * ↑π * I * (↑i / ↑n)) = exp (2 * ↑π * I / ↑n) ^ i
rw [← exp_nat_mul]
case mp.intro.intro.e_z
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
i : ℕ
hi : i < n
h : IsPrimitiveRoot (exp (2 * ↑π * I / ↑n) ^ i) n
⊢ 2 * ↑π * I * (↑i / ↑n) = ↑i * (2 * ↑π * I / ↑n)
case mp.intro.intro
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
i : ℕ
hi : i < n
h : IsPrimitiveRoot (exp (2 * ↑π * I / ↑n) ^ i) n
⊢ exp (2 * ↑π * I * (↑i / ↑n)) = exp (↑i * (2 * ↑π * I / ↑n))
congr 1
no goals
case mp.intro.intro.e_z
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
i : ℕ
hi : i < n
h : IsPrimitiveRoot (exp (2 * ↑π * I / ↑n) ^ i) n
⊢ 2 * ↑π * I * (↑i / ↑n) = ↑i * (2 * ↑π * I / ↑n)
field_simp [hn0, mul_comm (i : ℂ)]
no goals
ζ : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0
exact_mod_cast hn
case mpr.intro.intro.intro
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
i : ℕ
hi : Nat.coprime i n
⊢ IsPrimitiveRoot (exp (2 * ↑π * I * (↑i / ↑n))) n
case mpr
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (∃ i, i < n ∧ ∃ x, exp (2 * ↑π * I * (↑i / ↑n)) = ζ) → IsPrimitiveRoot ζ n
rintro ⟨i, -, hi, rfl⟩
no goals
case mpr.intro.intro.intro
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
i : ℕ
hi : Nat.coprime i n
⊢ IsPrimitiveRoot (exp (2 * ↑π * I * (↑i / ↑n))) n
exact isPrimitiveRoot_exp_of_coprime i n hn hi