instFintypeSubtypeUnitsRingOfIntegersMemSubgroupTorsion

English

Let K be a number field. The torsion subgroup of the units of the ring of integers of K is finite.

Русский

Пусть K — число поле. Торсионная подгруппа единиц кольца целых алгебра(K) конечна.

LaTeX

$$$\#(\mathrm{torsion}(K)) < \infty$$$

Lean4

/-- The torsion subgroup is finite. -/
instance : Fintype (torsion K) :=
  by
  refine @Fintype.ofFinite _ (Set.finite_coe_iff.mpr ?_)
  refine Set.Finite.of_finite_image ?_ (coe_injective K).injOn
  refine (Embeddings.finite_of_norm_le K ℂ 1).subset (fun a ⟨u, ⟨h_tors, h_ua⟩⟩ => ⟨?_, fun φ => ?_⟩)
  · rw [← h_ua]
    exact u.val.prop
  · rw [← h_ua]
    exact le_of_eq ((eq_iff_eq _ 1).mp ((mem_torsion K).mp h_tors) φ)

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