rootsOfUnity_eq_torsion — Mathlib

English

The group of roots of unity of order torsionOrder(K) equals the torsion subgroup.

Русский

Группа корней единицы порядка torsionOrder(K) совпадает с торсионной подгруппой.

LaTeX

$$$\mathrm{rootsOfUnity}(\mathrm{torsionOrder}(K), \mathcal{O}_K) = \mathrm{torsion}(K)$$$

Lean4

/-- The group of roots of unity of order dividing `torsionOrder` is equal to the torsion
group. -/
theorem rootsOfUnity_eq_torsion : rootsOfUnity (torsionOrder K) (𝓞 K) = torsion K :=
  by
  ext ζ
  rw [torsion, mem_rootsOfUnity]
  refine ⟨fun h => ?_, fun h => ?_⟩
  · rw [CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
    exact ⟨torsionOrder K, torsionOrder_pos K, h⟩
  · exact Subtype.ext_iff.mp (@pow_card_eq_one (torsion K) _ _ ⟨ζ, h⟩)

Похожие утверждения