instWfDvdMonoidIdeal — Mathlib

English

The divisor monoid of ideals is well-founded: there is no infinite descending chain of divisibility among ideals.

Русский

Делительный моноид идеалов является хорошо основанным: не существует бесконечной нисходящей цепи по делимости среди идеалов.

LaTeX

$$$\mathrm{WfDvdMonoid}(\mathrm{Ideal}(A))$$$

Lean4

instance : WfDvdMonoid (Ideal A) where
  wf := by
    have : WellFoundedGT (Ideal A) := inferInstance
    convert this.wf
    ext
    rw [Ideal.dvdNotUnit_iff_lt]

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