English
A complex number ζ is a primitive nth root of unity iff there exist i with 0 ≤ i < n and gcd(i, n) = 1 such that ζ = exp(2πi i/n).
Русский
Число ζ является примитивным корнем единицы порядка n тогда и только тогда, когда существует i, 0 ≤ i < n и gcd(i,n)=1, такое что ζ = exp(2πi i/n).
LaTeX
$$$IsPrimitiveRoot(\zeta, n) \iff \exists i < n, gcd(i,n)=1 \land exp(2\pi i i/n) = \zeta$$$
Lean4
theorem isPrimitiveRoot_iff (ζ : ℂ) (n : ℕ) (hn : n ≠ 0) :
IsPrimitiveRoot ζ n ↔ ∃ i < n, ∃ _ : i.Coprime n, exp (2 * π * I * (i / n)) = ζ :=
by
have hn0 : (n : ℂ) ≠ 0 := mod_cast hn
constructor; swap
· rintro ⟨i, -, hi, rfl⟩; exact isPrimitiveRoot_exp_of_coprime i n hn hi
intro h
have : NeZero n := ⟨hn⟩
obtain ⟨i, hi, rfl⟩ := (isPrimitiveRoot_exp n hn).eq_pow_of_pow_eq_one h.pow_eq_one
refine ⟨i, hi, ((isPrimitiveRoot_exp n hn).pow_iff_coprime (Nat.pos_of_ne_zero hn) i).mp h, ?_⟩
rw [← exp_nat_mul]
congr 1
field_simp
