Commit 2026-02-09 12:52 71cd708d

View on Github →

feat(RingTheory): Class Group of a Unique Factorization Domain is trivial (#33744) Add a theorem that the class group of a unique factorization domain is trivial. Together with the PR relating ClassGroup to PicardGroup, this will close a TODO in Mathlib.RingTheory.PicardGroup that the Picard Group of a UFD is trivial.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/ClassGroup.lean

added theorem ClassGroup.isPrincipal_coeSubmodule_of_isUnit

added theorem ClassGroup.isPrincipal_of_isUnit_coeIdeal

added theorem FractionalIdeal.isUnit_num

Modified Mathlib/RingTheory/FractionalIdeal/Operations.lean

added theorem FractionalIdeal.isPrincipal_of_isPrincipal_num

Modified Mathlib/RingTheory/PicardGroup.lean

Created Mathlib/RingTheory/UniqueFactorizationDomain/ClassGroup.lean

added theorem NormalizedGCDMonoid.isPrincipal_of_exists_mul_ne_zero_isPrincipal