normalizedFactors_prod_of_prime — Mathlib

English

If a finite multiset m of α contains only primes and units are trivial, then normalizedFactors of prod m equals m.

Русский

Если конечное мульти‑множество m из α состоит только из простых и единицы тривиальны, то нормализованные факторы произведения prod m равны m.

LaTeX

$$normalizedFactors.prod m = m \text{ given } (∀ p ∈ m, Prime p) \land [Subsingleton (Units α)]$$

Lean4

theorem normalizedFactors_prod_of_prime [Subsingleton αˣ] {m : Multiset α} (h : ∀ p ∈ m, Prime p) :
    normalizedFactors m.prod = m := by
  cases subsingleton_or_nontrivial α
  · obtain rfl : m = 0 := by
      refine Multiset.eq_zero_of_forall_notMem fun x hx ↦ ?_
      simpa [Subsingleton.elim x 0] using h x hx
    simp
  ·
    simpa only [← Multiset.rel_eq, ← associated_eq_eq] using
      prime_factors_unique prime_of_normalized_factor h (prod_normalizedFactors (m.prod_ne_zero_of_prime h))

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