card_classGroup_eq_one — Mathlib

English

For a principal ideal ring, the class group is a singleton; equivalently, the class number is 1.

Русский

Для кольца с главными идеалами класс-группа тривиальна; иначе говоря, класс-число равно 1.

LaTeX

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

Lean4

/-- The class number of a principal ideal domain is `1`. -/
theorem card_classGroup_eq_one [IsPrincipalIdealRing R] : Fintype.card (ClassGroup R) = 1 :=
  by
  rw [Fintype.card_eq_one_iff]
  use 1
  refine ClassGroup.induction (R := R) (FractionRing R) (fun I => ?_)
  exact ClassGroup.mk_eq_one_iff.mpr (I : FractionalIdeal R⁰ (FractionRing R)).isPrincipal

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