English
For a primitive nth root ζ of unity with n > 0, there exists an integer i with gcd(i,n)=1 and |i| < n such that ζ.arg = (2π i)/n.
Русский
Для примитивного n-го корня ζ единицы существует целое число i, взаимно простое с n, и |i| < n, такое что arg(ζ) = (2π i)/n.
LaTeX
$$IsPrimitiveRoot.arg: ∃ i ∈ ℤ, ζ.arg = (i / n) * (2 π) ∧ IsCoprime i n ∧ |i| < n$$
Lean4
theorem arg {n : ℕ} {ζ : ℂ} (h : IsPrimitiveRoot ζ n) (hn : n ≠ 0) :
∃ i : ℤ, ζ.arg = i / n * (2 * Real.pi) ∧ IsCoprime i n ∧ i.natAbs < n :=
by
rw [Complex.isPrimitiveRoot_iff _ _ hn] at h
obtain ⟨i, h, hin, rfl⟩ := h
rw [mul_comm, ← mul_assoc, Complex.exp_mul_I]
refine ⟨if i * 2 ≤ n then i else i - n, ?_, ?isCoprime, by cutsat⟩
case isCoprime =>
replace hin := Nat.isCoprime_iff_coprime.mpr hin
split_ifs
· exact hin
· convert hin.add_mul_left_left (-1) using 1
rw [mul_neg_one, sub_eq_add_neg]
split_ifs with h₂
· convert Complex.arg_cos_add_sin_mul_I _
· push_cast; rfl
· push_cast; rfl
simp only [Int.cast_natCast, Set.mem_Ioc]
refine ⟨(neg_lt_neg Real.pi_pos).trans_le ?_, ?_⟩
· rw [neg_zero]
positivity
refine Eq.trans_le (b := Real.pi * (i * 2 / n)) (by ring) ?_
rw [← mul_one n] at h₂
exact mul_le_of_le_one_right Real.pi_pos.le ((div_le_iff₀' <| mod_cast pos_of_gt h).mpr <| mod_cast h₂)
rw [← Complex.cos_sub_two_pi, ← Complex.sin_sub_two_pi]
convert Complex.arg_cos_add_sin_mul_I _
· push_cast
rw [← sub_one_mul, sub_div, div_self]
exact mod_cast hn
· push_cast
rw [← sub_one_mul, sub_div, div_self]
exact mod_cast hn
simp only [Int.cast_sub, Int.cast_natCast, Set.mem_Ioc]
field_simp
constructor
· push_neg at h₂
rify at h₂
linear_combination h₂
· rify at h
linear_combination 2 * h + (n : ℝ) * one_pos (α := ℝ)
