theorem IsDedekindDomain.uniqueFactorizationMonoid_iff_isPrincipalIdealRing (R : Type u_1) [CommRing R] [IsDedekindDomain R] : UniqueFactorizationMonoid R ↔ IsPrincipalIdealRing R

theorem IsDedekindDomain.isPrincipalIdealRing_iff_subsingleton_classGroup (R : Type u_1) [CommRing R] [IsDedekindDomain R] : IsPrincipalIdealRing R ↔ Subsingleton (ClassGroup R)

theorem IsDedekindDomain.uniqueFactorizationMonoid_iff_subsingleton_classGroup (R : Type u_1) [CommRing R] [IsDedekindDomain R] : UniqueFactorizationMonoid R ↔ Subsingleton (ClassGroup R)