The class group of a Unique Factorization Domain is trivial #
This file proves that the ideal class group of a GCD Domain is trivial. The main application is to Unique Factorization Domains, which are known to be GCD Domains.
Main result #
IsGCDMonoid.subsingleton_classGroup: the class group of a GCD domain is trivial. This includes unique factorization domains.
References #
theorem IsGCDMonoid.isPrincipal_of_exists_mul_ne_zero_isPrincipal {R : Type u_1} [CommRing R] [IsDomain R] [IsGCDMonoid R] {J : Ideal R} (hJ : ∃ (K : Ideal R), J * K ≠ 0 ∧ Submodule.IsPrincipal (J * K)) :
instance IsGCDMonoid.subsingleton_classGroup {R : Type u_1} [CommRing R] [IsDomain R] [IsGCDMonoid R] :
The ideal class group of a GCD domain is trivial. This includes unique factorization domains.
@[deprecated IsGCDMonoid.isPrincipal_of_exists_mul_ne_zero_isPrincipal (since := "2026-07-08")]
theorem NormalizedGCDMonoid.isPrincipal_of_exists_mul_ne_zero_isPrincipal {R : Type u_1} [CommRing R] [IsDomain R] [IsGCDMonoid R] {J : Ideal R} (hJ : ∃ (K : Ideal R), J * K ≠ 0 ∧ Submodule.IsPrincipal (J * K)) :
Alias of IsGCDMonoid.isPrincipal_of_exists_mul_ne_zero_isPrincipal.