decompositionMonoid_iff — Mathlib

English

For any commutative monoid M, DecompositionMonoid(Associates M) holds if and only if DecompositionMonoid M holds.

Русский

Для любого коммутативного моноида M условие разложимости для Associates M эквивалентно условию разложимости самого M.

LaTeX

$$$ \operatorname{DecompositionMonoid}(\mathrm{Associates}(M)) \iff \operatorname{DecompositionMonoid}(M) $$$

Lean4

@[simp]
theorem decompositionMonoid_iff : DecompositionMonoid (Associates M) ↔ DecompositionMonoid M := by
  simp_rw [_root_.decompositionMonoid_iff, forall_associated, isPrimal_mk]

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