Unique factorization and ascending chain condition on ideals #
Main results #
Ideal.setOfPred_isPrincipal_wellFoundedOn_gt,WfDvdMonoid.of_setOfPred_isPrincipal_wellFoundedOn_gtin a domain, well-foundedness of the strict version of ∣ is equivalent to the ascending chain condition on principal ideals.
theorem Ideal.IsPrime.exists_mem_prime_of_ne_bot {R : Type u_2} [CommSemiring R] [UniqueFactorizationMonoid R] {I : Ideal R} (hI₂ : I.IsPrime) (hI : I ≠ ⊥) :
∃ x ∈ I, Prime x
Every non-zero prime ideal in a unique factorization domain contains a prime element.
theorem Ideal.setOfPred_isPrincipal_wellFoundedOn_gt {α : Type u_1} [CommSemiring α] [WfDvdMonoid α] [IsDomain α] :
{I : Ideal α | Submodule.IsPrincipal I}.WellFoundedOn fun (x1 x2 : Ideal α) => x1 > x2
The ascending chain condition on principal ideals holds in a WfDvdMonoid domain.
@[deprecated Ideal.setOfPred_isPrincipal_wellFoundedOn_gt (since := "2026-07-09")]
theorem Ideal.setOf_isPrincipal_wellFoundedOn_gt {α : Type u_1} [CommSemiring α] [WfDvdMonoid α] [IsDomain α] :
{I : Ideal α | Submodule.IsPrincipal I}.WellFoundedOn fun (x1 x2 : Ideal α) => x1 > x2
Alias of Ideal.setOfPred_isPrincipal_wellFoundedOn_gt.
The ascending chain condition on principal ideals holds in a WfDvdMonoid domain.
theorem WfDvdMonoid.of_setOfPred_isPrincipal_wellFoundedOn_gt {α : Type u_1} [CommSemiring α] [IsDomain α] (h : {I : Ideal α | Submodule.IsPrincipal I}.WellFoundedOn fun (x1 x2 : Ideal α) => x1 > x2) :
The ascending chain condition on principal ideals in a domain is sufficient to prove that
the domain is WfDvdMonoid.
@[deprecated WfDvdMonoid.of_setOfPred_isPrincipal_wellFoundedOn_gt (since := "2026-07-09")]
theorem WfDvdMonoid.of_setOf_isPrincipal_wellFoundedOn_gt {α : Type u_1} [CommSemiring α] [IsDomain α] (h : {I : Ideal α | Submodule.IsPrincipal I}.WellFoundedOn fun (x1 x2 : Ideal α) => x1 > x2) :
Alias of WfDvdMonoid.of_setOfPred_isPrincipal_wellFoundedOn_gt.
The ascending chain condition on principal ideals in a domain is sufficient to prove that
the domain is WfDvdMonoid.