i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
⊢ exp (2 * ↑π * I * (↑i / ↑n)) ^ n = 1 ∧ ∀ (l : ℕ), exp (2 * ↑π * I * (↑i / ↑n)) ^ l = 1 → n ∣ l
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
⊢ IsPrimitiveRoot (exp (2 * ↑π * I * (↑i / ↑n))) n
rw [IsPrimitiveRoot.iff_def]
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
⊢ (∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) ∧
    ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
⊢ exp (2 * ↑π * I * (↑i / ↑n)) ^ n = 1 ∧ ∀ (l : ℕ), exp (2 * ↑π * I * (↑i / ↑n)) ^ l = 1 → n ∣ l
simp only [← exp_nat_mul, exp_eq_one_iff]
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
⊢ (∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) ∧
    ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
⊢ (∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) ∧
    ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l
have hn0 : (n : ℂ) ≠ 0 := by exact_mod_cast h0
case left
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
⊢ ∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)

case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
⊢ ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
⊢ (∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) ∧
    ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l
constructor
no goals
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
⊢ ↑n ≠ 0
exact_mod_cast h0
case left
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
⊢ ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑↑i * (2 * ↑π * I)
case left
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
⊢ ∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)
use i
no goals
case left
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
⊢ ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑↑i * (2 * ↑π * I)
field_simp [hn0, mul_comm (i : ℂ), mul_comm (n : ℂ)]
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
⊢ ∀ (l : ℕ) (x : ℤ), ↑i * ↑l * (2 * ↑π * I) = ↑x * (2 * ↑π * I) * ↑n → n ∣ l
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
⊢ ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l
simp only [hn0, mul_right_comm _ _ ↑n, mul_left_inj' two_pi_I_ne_zero, Ne.def, not_false_iff,
  mul_comm _ (i : ℂ), ← mul_assoc _ (i : ℂ), exists_imp, field_simps]
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
⊢ ∀ (l : ℕ) (x : ℤ), ↑(i * l) * (↑(2 * π) * I) = ↑x * (↑(2 * π) * I) * ↑n → n ∣ l
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
⊢ ∀ (l : ℕ) (x : ℤ), ↑i * ↑l * (2 * ↑π * I) = ↑x * (2 * ↑π * I) * ↑n → n ∣ l
norm_cast
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑k * (↑(2 * π) * I) * ↑n
⊢ n ∣ l
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
⊢ ∀ (l : ℕ) (x : ℤ), ↑(i * l) * (↑(2 * π) * I) = ↑x * (↑(2 * π) * I) * ↑n → n ∣ l
rintro l k hk
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑n * ↑k * (↑(2 * π) * I)
⊢ n ∣ l
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑k * (↑(2 * π) * I) * ↑n
⊢ n ∣ l
conv_rhs at hk => rw [mul_comm, ← mul_assoc]
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑n * ↑k * (↑(2 * π) * I)
hz : 2 * ↑π * I ≠ 0
⊢ n ∣ l
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑n * ↑k * (↑(2 * π) * I)
⊢ n ∣ l
have hz : 2 * ↑π * I ≠ 0 := by simp [pi_pos.ne.symm, I_ne_zero]
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑i * ↑l = ↑n * ↑k
⊢ n ∣ l
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑n * ↑k * (↑(2 * π) * I)
hz : 2 * ↑π * I ≠ 0
⊢ n ∣ l
field_simp [hz] at hk
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑(i * l) = ↑n * k
⊢ n ∣ l
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑i * ↑l = ↑n * ↑k
⊢ n ∣ l
norm_cast at hk
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑(i * l) = ↑n * k
this : n ∣ i * l
⊢ n ∣ l
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑(i * l) = ↑n * k
⊢ n ∣ l
have : n ∣ i * l := by rw [← Int.coe_nat_dvd, hk, mul_comm]; apply dvd_mul_left
no goals
case right
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑(i * l) = ↑n * k
this : n ∣ i * l
⊢ n ∣ l
exact hi.symm.dvd_of_dvd_mul_left this
no goals
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑n * ↑k * (↑(2 * π) * I)
⊢ 2 * ↑π * I ≠ 0
simp [pi_pos.ne.symm, I_ne_zero]
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑(i * l) = ↑n * k
⊢ ↑n ∣ k * ↑n
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑(i * l) = ↑n * k
⊢ n ∣ i * l
rw [← Int.coe_nat_dvd, hk, mul_comm]
no goals
i n : ℕ
h0 : n ≠ 0
hi : Nat.coprime i n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑(i * l) = ↑n * k
⊢ ↑n ∣ k * ↑n
apply dvd_mul_left