of_setOf_isPrincipal_wellFoundedOn_gt

English

If the set of principal ideals is well-founded, then the domain is a WfDvdMonoid.

Русский

Если множество главных идеалов хорошо обосновано, то домен является WfDvdMonoid.

LaTeX

$$$\\text{If } {\\alpha} \\text{ is such that } {I : \\text{Ideal } \\alpha \\mid I.IsPrincipal}.\\WellFoundedOn (>), \\text{ then } \\alpha \\text{ is a } WfDvdMonoid$$$

Lean4

/-- The ascending chain condition on principal ideals in a domain is sufficient to prove that
the domain is `WfDvdMonoid`. -/
theorem of_setOf_isPrincipal_wellFoundedOn_gt [CommSemiring α] [IsDomain α]
    (h : {I : Ideal α | I.IsPrincipal}.WellFoundedOn (· > ·)) : WfDvdMonoid α :=
  by
  have : WellFounded (α := { I : Ideal α // I.IsPrincipal }) (· > ·) := h
  constructor
  convert InvImage.wf (fun a => ⟨Ideal.span ({ a } : Set α), _, rfl⟩) this
  ext
  exact Ideal.span_singleton_lt_span_singleton.symm

Похожие утверждения