mem_normalizedFactors_iff — Mathlib

English

If all elements of a multiset m are prime, then the normalized factors of the product of m equal m (under a mild unit-condition).

Русский

Если все элементыmultiset m — простые, то нормализованные факторы произведения m равны m (при разумном условии об единицах).

LaTeX

$$normalizedFactors m.prod = m$$

Lean4

theorem mem_normalizedFactors_iff [Subsingleton αˣ] {p x : α} (hx : x ≠ 0) :
    p ∈ normalizedFactors x ↔ Prime p ∧ p ∣ x := by
  constructor
  · intro h
    exact ⟨prime_of_normalized_factor p h, dvd_of_mem_normalizedFactors h⟩
  · rintro ⟨hprime, hdvd⟩
    obtain ⟨q, hqmem, hqeq⟩ := exists_mem_normalizedFactors_of_dvd hx hprime.irreducible hdvd
    rw [associated_iff_eq] at hqeq
    exact hqeq ▸ hqmem

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