instFintypeClassGroupOfIsPrincipalIdealRing

English

The class group of a principal ideal ring is a singleton; i.e., it contains exactly one element.

Русский

Класс-группа кольца с принципиальными идеалами является единичным множеством; в ней ровно один элемент.

LaTeX

$$$|\mathrm{Cl}(R)| = 1$$$

Lean4

/-- The class group of principal ideal domain is finite (in fact a singleton).

See `ClassGroup.fintypeOfAdmissibleOfFinite` for a finiteness proof that works for rings of integers
of global fields.
-/
noncomputable instance [IsPrincipalIdealRing R] : Fintype (ClassGroup R)
    where
  elems := { 1 }
  complete := by
    refine ClassGroup.induction (R := R) (FractionRing R) (fun I => ?_)
    rw [Finset.mem_singleton]
    exact ClassGroup.mk_eq_one_iff.mpr (I : FractionalIdeal R⁰ (FractionRing R)).isPrincipal

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