Consequences of Krull's Height Theorem

theorem UniqueFactorizationMonoid.isPrincipal_of_height_eq_one {R : Type u_1} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] (p : Ideal R) [p.IsPrime] (h : p.height = 1) : Submodule.IsPrincipal p

Every height one prime ideal in a UFD is principal.

theorem UniqueFactorizationMonoid.of_primeHeight_eq_one_imp_isPrincipal (R : Type u_1) [CommRing R] [IsDomain R] [IsNoetherianRing R] (h : ∀ (p : PrimeSpectrum R), p.asIdeal.primeHeight = 1 → Submodule.IsPrincipal p.asIdeal) : UniqueFactorizationMonoid R

A Noetherian domain whose height one prime ideals are principal is a UFD.

theorem IsNoetherianRing.uniqueFactorizationMonoid_iff (R : Type u_1) [CommRing R] [IsDomain R] [IsNoetherianRing R] : UniqueFactorizationMonoid R ↔ ∀ (p : PrimeSpectrum R), p.asIdeal.primeHeight = 1 → Submodule.IsPrincipal p.asIdeal

A Noetherian domain is a UFD if and only if every height one prime ideal is principal.