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.