English
In a cyclotomic extension of ℚ, if there exists a primitive l-th root of unity and l ≠ 0, then l divides 2n.
Русский
В циклотомическом расширении ℚ существует примитивный l-й корень, и l ≠ 0; тогда l делится на 2n.
LaTeX
$$$$ l \mid 2n $$$$
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 exist `r`
such that `x = (-ζ)^r`. -/
theorem exists_neg_pow_of_isOfFinOrder [IsCyclotomicExtension { n } ℚ K] (hno : Odd n) {ζ x : K}
(hζ : IsPrimitiveRoot ζ n) (hx : IsOfFinOrder x) : ∃ r : ℕ, x = (-ζ) ^ r :=
by
have hnegζ : IsPrimitiveRoot (-ζ) (2 * n) :=
by
convert IsPrimitiveRoot.orderOf (-ζ)
rw [neg_eq_neg_one_mul, (Commute.all _ _).orderOf_mul_eq_mul_orderOf_of_coprime]
· simp [hζ.eq_orderOf]
· simp [← hζ.eq_orderOf, hno]
obtain ⟨k, hkpos, hkn⟩ := isOfFinOrder_iff_pow_eq_one.1 hx
obtain ⟨l, hl, hlroot⟩ := (isRoot_of_unity_iff hkpos _).1 hkn
have hlzero : NeZero l := ⟨fun h ↦ by simp [h] at hl⟩
have : NeZero (l : K) := ⟨NeZero.natCast_ne l K⟩
rw [isRoot_cyclotomic_iff] at hlroot
obtain ⟨a, ha⟩ := hlroot.dvd_of_isCyclotomicExtension n hlzero.1
replace hlroot : x ^ (2 * n) = 1 := by rw [ha, pow_mul, hlroot.pow_eq_one, one_pow]
obtain ⟨s, -, hs⟩ := hnegζ.eq_pow_of_pow_eq_one hlroot
exact ⟨s, hs.symm⟩
