mem_normalizedFactors_iff' — Mathlib

English

If a and b occur as elements of normalizedFactors(c) and are associated, then a = b.

Русский

Если a и b входят в normalizedFactors(c) и ассоциированы, то a = b.

LaTeX

$$Multiset.instMembership.mem (normalizedFactors c) a \land Multiset.instMembership.mem (normalizedFactors c) b \land Associated a b → a = b$$

Lean4

theorem mem_normalizedFactors_iff' {p x : α} (h : x ≠ 0) :
    p ∈ normalizedFactors x ↔ Irreducible p ∧ normalize p = p ∧ p ∣ x :=
  by
  refine
    ⟨fun h ↦ ⟨irreducible_of_normalized_factor p h, normalize_normalized_factor p h, dvd_of_mem_normalizedFactors h⟩,
      fun ⟨h₁, h₂, h₃⟩ ↦ ?_⟩
  obtain ⟨y, hy₁, hy₂⟩ := exists_mem_factors_of_dvd h h₁ h₃
  exact Multiset.mem_map.mpr ⟨y, hy₁, by rwa [← h₂, normalize_eq_normalize_iff_associated, Associated.comm]⟩

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