ufm — Mathlib

English

Under suitable assumptions, the associates form a unique factorization monoid.

Русский

При определённых предпосылках ассоциированные образуют уникальный факторизационный моноид.

LaTeX

$$Associates.ufm$$

Lean4

instance ufm [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] : UniqueFactorizationMonoid (Associates α) :=
  { (WfDvdMonoid.wfDvdMonoid_associates : WfDvdMonoid (Associates α)) with
    irreducible_iff_prime := by
      rw [← Associates.irreducible_iff_prime_iff]
      apply UniqueFactorizationMonoid.irreducible_iff_prime }

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