ufm_of_decomposition_of_wfDvdMonoid

English

If α is a CancelCommMonoidWithZero, a WfDvdMonoid, and a DecompositionMonoid, then α is a Unique Factorization Monoid.

Русский

Если α — CancelCommMonoidWithZero, WfDvdMonoid и DecompositionMonoid, тогда α является моноидом с единственным факторизованием.

LaTeX

$$$[\text{CancelCommMonoidWithZero }\alpha] \,[WfDvdMonoid\alpha] \,[DecompositionMonoid\alpha] \Rightarrow \mathrm{UniqueFactorizationMonoid}\alpha.$$$

Lean4

instance (priority := 100) ufm_of_decomposition_of_wfDvdMonoid [CancelCommMonoidWithZero α] [WfDvdMonoid α]
    [DecompositionMonoid α] : UniqueFactorizationMonoid α :=
  { ‹WfDvdMonoid α› with irreducible_iff_prime := irreducible_iff_prime }

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