English
For a Dedekind domain R with a finite class group, the class group has one element if and only if R is a principal ideal ring.
Русский
Для дедекиндового кольца R с конечной класс-группой, число классов равно единице тогда и только тогда, когда R имеет принципиальные идеалы (главных идеалов нетрудно добиться).
LaTeX
$$$|\mathrm{Cl}(R)| = 1 \iff \text{IsPrincipalIdealRing}(R)$$$
Lean4
/-- The class number is `1` iff the ring of integers is a principal ideal domain. -/
theorem card_classGroup_eq_one_iff [IsDedekindDomain R] [Fintype (ClassGroup R)] :
Fintype.card (ClassGroup R) = 1 ↔ IsPrincipalIdealRing R :=
by
constructor; swap; · intros; convert card_classGroup_eq_one (R := R)
rw [Fintype.card_eq_one_iff]
rintro ⟨I, hI⟩
have eq_one : ∀ J : ClassGroup R, J = 1 := fun J => (hI J).trans (hI 1).symm
refine ⟨fun I => ?_⟩
by_cases hI : I = ⊥
· rw [hI]; exact bot_isPrincipal
· exact (ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_iff_ne_zero.mpr hI)).mp (eq_one _)
