Consequences of Krull's Height Theorem

The results in this file were already in mathlib (with different names).

@[deprecated UniqueFactorizationMonoid.of_forall_isPrincipal_of_height_eq_one (since := "2026-07-25")]

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

Alias of UniqueFactorizationMonoid.of_forall_isPrincipal_of_height_eq_one.

@[deprecated UniqueFactorizationMonoid.iff_forall_isPrincipal_of_height_eq_one (since := "2026-07-25")]

theorem IsNoetherianRing.uniqueFactorizationMonoid_iff {R : Type u_1} [CommRing R] [IsDomain R] [IsNoetherianRing R] : UniqueFactorizationMonoid R ↔ ∀ (p : Ideal R) [p.IsPrime], p.height = 1 → Submodule.IsPrincipal p

Alias of UniqueFactorizationMonoid.iff_forall_isPrincipal_of_height_eq_one.