instDecompositionMonoid — Mathlib

English

Under suitable hypotheses, a unique factorization monoid structure yields a decomposition monoid structure.

Русский

При подходящих гипотезах уникального факторизационного моноида структура переходит в структуру разложимого моноида.

LaTeX

$$Instance: DecompositionMonoid α where primal a := ...$$

Lean4

instance : DecompositionMonoid α where
  primal
    a := by
    obtain rfl | ha := eq_or_ne a 0; · exact isPrimal_zero
    obtain ⟨f, hf, u, rfl⟩ := exists_prime_factors a ha
    exact ((Submonoid.isPrimal α).multiset_prod_mem f (hf · · |>.isPrimal)).mul u.isUnit.isPrimal

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