wellFoundedLT_associates — Mathlib

English

There is a well-founded linear order on the associates with respect to lt given by the divisibility relation.

Русский

На ассоциированных существует хорошо упорядованные линейно отношение порядка lt по делимости.

LaTeX

$$wellFoundedLT(Associates α)$$

Lean4

theorem wellFoundedLT_associates : WellFoundedLT (Associates α) :=
  ⟨Subrelation.wf dvdNotUnit_of_lt wellFounded_dvdNotUnit⟩

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