factors_multiset_prod_of_irreducible

English

If s is a multiset of naturals and every element of s is irreducible, then normalizedFactors of prod s equals s.

Русский

Если s — многосет натуральных чисел, и каждый элемент s неразложим, то нормализованные факторы произведения s равны самому s.

LaTeX

$$normalizedFactors(s.prod) = s$$

Lean4

theorem factors_multiset_prod_of_irreducible {s : Multiset ℕ} (h : ∀ x : ℕ, x ∈ s → Irreducible x) :
    normalizedFactors s.prod = s := by
  rw [← Multiset.rel_eq, ← associated_eq_eq]
  apply UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor h (prod_normalizedFactors _)
  rw [Ne, Multiset.prod_eq_zero_iff]
  exact fun con ↦ not_irreducible_zero (h 0 con)

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