English
Let n be an odd positive integer. Suppose x is a root of unity in an n-th cyclotomic extension of Q, and ζ is a primitive n-th root of unity in the same extension. Then there exists an integer r with 0 ≤ r < n such that x = ζ^r or x = −ζ^r.
Русский
Пусть n — нечетное натуральное число. Пусть x — корень единицы в n-ой циклотомической области над Q, и ζ — примитивный n-ый корень единицы в той же области. Тогда существует целое число r с 0 ≤ r < n такое, что x = ζ^r или x = −ζ^r.
LaTeX
$$$\exists r \in \{0,1,\dots,n-1\}: x = \zeta^{r} \ \\lor\ x = -\zeta^{r}$$$
Lean4
/-- If `x` is a root of unity (spelled as `IsOfFinOrder x`) in an `n`-th cyclotomic extension of
`ℚ`, where `n` is odd, and `ζ` is a primitive `n`-th root of unity, then there exists `r < n`
such that `x = ζ^r` or `x = -ζ^r`. -/
theorem exists_pow_or_neg_mul_pow_of_isOfFinOrder [IsCyclotomicExtension { n } ℚ K] (hno : Odd n) {ζ x : K}
(hζ : IsPrimitiveRoot ζ n) (hx : IsOfFinOrder x) : ∃ r : ℕ, r < n ∧ (x = ζ ^ r ∨ x = -ζ ^ r) :=
by
obtain ⟨r, hr⟩ := hζ.exists_neg_pow_of_isOfFinOrder hno hx
refine ⟨r % n, Nat.mod_lt _ (NeZero.pos _), ?_⟩
rw [show ζ ^ (r % n) = ζ ^ r from (IsPrimitiveRoot.eq_orderOf hζ).symm ▸ pow_mod_orderOf .., hr]
rcases Nat.even_or_odd r with (h | h) <;> simp [neg_pow, h.neg_one_pow]
