mem_normalizedFactors_eq_of_associated

English

If a and b occur in 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_eq_of_associated {a b c : α} (ha : a ∈ normalizedFactors c) (hb : b ∈ normalizedFactors c)
    (h : Associated a b) : a = b :=
  by
  rw [← normalize_normalized_factor a ha, ← normalize_normalized_factor b hb, normalize_eq_normalize_iff]
  exact Associated.dvd_dvd h

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