iff_exists_prime_factors — Mathlib

English

There is a correspondence between prime factor decompositions up to association for irreducibles, yielding a unique factorization monoid.

Русский

Существует соответствие разложения на простые до ассоциаций между мультисетами ирредуцируемых.

LaTeX

$$$\forall a \; (\mathrm{Irreducible}(a) \Rightarrow \mathrm{Prime}(a)) \Rightarrow \mathrm{UniqueFactorizationMonoid}(\alpha).$$$

Lean4

theorem iff_exists_prime_factors [CancelCommMonoidWithZero α] :
    UniqueFactorizationMonoid α ↔ ∀ a : α, a ≠ 0 → ∃ f : Multiset α, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a :=
  ⟨fun h => @UniqueFactorizationMonoid.exists_prime_factors _ _ h, UniqueFactorizationMonoid.of_exists_prime_factors⟩

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