of_wfDvdMonoid_associates — Mathlib

English

The well-foundedness of the divisor relation on associates is inherited from the base ring structure.

Русский

Упорядоченная по делимости связь на ассоциированных элементах наследуется от базовой структуры кольца.

LaTeX

$$WfDvdMonoid.of_wfDvdMonoid_associates$$

Lean4

theorem of_wfDvdMonoid_associates (_ : WfDvdMonoid (Associates α)) : WfDvdMonoid α :=
  ⟨(mk_surjective.wellFounded_iff mk_dvdNotUnit_mk_iff.symm).2 wellFounded_dvdNotUnit⟩

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