Commit 2026-06-29 08:56 e752928d

feat(RingTheory): UFD criteria via height 1 prime ideals and localization (#36739) We prove the following UFD criteria via height 1 prime ideals and localization:

1. Let R be a Noetherian domain. Then R is a UFD if and only if every height 1 prime ideal is principal.
2. Let R be a Noetherian domain, x ∈ R be a prime element. If Rₓ is a UFD, then R is also a UFD.