Theorems · Theorem · commutative algebra

WfDvdMonoid.of_setOfPred_isPrincipal_wellFoundedOn_gt

∀ {α : Type u_1} [inst : CommSemiring α] [IsDomain α],
  ({I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 => x1 > x2) → WfDvdMonoid α

The ascending chain condition on principal ideals in a domain is sufficient to prove that the domain is WfDvdMonoid.

Defined in: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Cited by: 1 results in Mathlib
Foundations: Depth 31 from the axioms · uses propext, Quot.sound
Assumes: CommSemiring IsDomain

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommSemiringstatement and proof · cited by 10,911
Set.ofPredstatement and proof · cited by 6,101
Idealstatement and proof · cited by 4,748
IsDomainstatement and proof · cited by 2,196
Ideal.spanproof · cited by 948
Submodule.IsPrincipalstatement and proof · cited by 129
Set.WellFoundedOnstatement and proof · cited by 53
WfDvdMonoidstatement · cited by 37
DvdNotUnitproof · cited by 33
Ideal.span_singleton_lt_span_singletonproof · cited by 4

Cited by1

Results whose statement or proof uses this declaration.

WfDvdMonoid.of_setOf_isPrincipal_wellFoundedOn_gtproof · cited by 0