instDecompositionMonoid

Mathlib.Algebra.GroupWithZero.Associated

URI: https://scilib.ai/kg/mathlib#Associates.instDecompositionMonoid

English

If M is a decomposition monoid, then Associates M is a decomposition monoid.

Русский

Если M — разложимый моноид, то Associates(M) — разложимый моноид.

LaTeX

$$$ [DecompositionMonoid](M) \Rightarrow DecompositionMonoid(Associates M) $$$

Lean4

instance instDecompositionMonoid [DecompositionMonoid M] : DecompositionMonoid (Associates M) :=
  decompositionMonoid_iff.mpr ‹_›

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

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

Разделы

Аффилиация

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