setOf_isPrincipal_wellFoundedOn_gt

English

The ascending chain condition on principal ideals holds in a WfDvdMonoid domain.

Русский

Условие восходящих цепей главных идеалов выполняется в домене WfDvdMonoid.

LaTeX

$$$\\text{setOf fun I => I.IsPrincipal}.\\text{WellFoundedOn} (\\cdot > \\cdot)$$$

Lean4

/-- The ascending chain condition on principal ideals holds in a `WfDvdMonoid` domain. -/
theorem setOf_isPrincipal_wellFoundedOn_gt [CommSemiring α] [WfDvdMonoid α] [IsDomain α] :
    {I : Ideal α | I.IsPrincipal}.WellFoundedOn (· > ·) :=
  by
  have : {I : Ideal α | I.IsPrincipal} = ((fun a ↦ Ideal.span { a }) '' Set.univ) :=
    by
    ext
    simp [Submodule.isPrincipal_iff, eq_comm]
  rw [this, Set.wellFoundedOn_image, Set.wellFoundedOn_univ]
  convert wellFounded_dvdNotUnit (α := α)
  ext
  exact Ideal.span_singleton_lt_span_singleton

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