iff_wellFounded_associates — Mathlib

English

A cancellation property plus well-foundedness is equivalent to well-founded divisibility on associates.

Русский

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

LaTeX

$$theorem iff_wellFounded_associates$$

Lean4

theorem iff_wellFounded_associates [CancelCommMonoidWithZero α] : WfDvdMonoid α ↔ WellFoundedLT (Associates α) :=
  ⟨by apply WfDvdMonoid.wellFoundedLT_associates, WfDvdMonoid.of_wellFoundedLT_associates⟩

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