normalizedFactors_eq — Mathlib

English

If two elements are associates, then their multisets of normalized factors are equal.

Русский

Если два элемента ассоциированы между собой, то их множества нормализованных факторов совпадают.

LaTeX

$$Associated(a,b) \rightarrow \operatorname{normalizedFactors}(a) = \operatorname{normalizedFactors}(b)$$

Lean4

theorem _root_.Associated.normalizedFactors_eq {a b : α} (h : Associated a b) :
    normalizedFactors a = normalizedFactors b :=
  by
  unfold normalizedFactors
  have h' : ⇑(normalize (α := α)) = Associates.out ∘ Associates.mk := funext Associates.out_mk
  rw [h', ← Multiset.map_map, ← Multiset.map_map,
    Associates.rel_associated_iff_map_eq_map.mp (factors_rel_of_associated h)]

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