English
If k is a positive integer coprime to the torsion order, then the only k-th root of unity in 𝓞_K is 1.
Русский
Если k — положительное число, взаимно простое с порядком торсионной подгруппы, то в 𝓞_K единственный корень единицы порядка k равен 1.
LaTeX
$$$\gcd(k, \mathrm{torsionOrder}(K)) = 1 \\Rightarrow \mathrm{rootsOfUnity}(k, \mathcal{O}_K) = \{1\}$$$
Lean4
/-- If `k` does not divide `torsionOrder` then there are no nontrivial roots of unity of
order dividing `k`. -/
theorem rootsOfUnity_eq_one {k : ℕ+} (hc : Nat.Coprime k (torsionOrder K)) {ζ : (𝓞 K)ˣ} :
ζ ∈ rootsOfUnity k (𝓞 K) ↔ ζ = 1 := by
rw [mem_rootsOfUnity]
refine ⟨fun h => ?_, fun h => by rw [h, one_pow]⟩
refine orderOf_eq_one_iff.mp (Nat.eq_one_of_dvd_coprimes hc ?_ ?_)
· exact orderOf_dvd_of_pow_eq_one h
· have hζ : ζ ∈ torsion K :=
by
rw [torsion, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
exact ⟨k, k.prop, h⟩
rw [orderOf_submonoid (⟨ζ, hζ⟩ : torsion K)]
exact orderOf_dvd_card
