wfDvdMonoid_associates

Mathlib.RingTheory.UniqueFactorizationDomain.Basic

URI: https://scilib.ai/kg/mathlib#WfDvdMonoid.wfDvdMonoid_associates

← MathLib Explorer

English

Associates form a well-founded divisible monoid under the divisor order.

Русский

Ассоциированные образуют хорошо упорядоченный по делимости моноид.

LaTeX

$$WfDvdMonoid.wfDvdMonoid_associates$$

Lean4

instance wfDvdMonoid_associates : WfDvdMonoid (Associates α) :=
  ⟨(mk_surjective.wellFounded_iff mk_dvdNotUnit_mk_iff.symm).1 wellFounded_dvdNotUnit⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru