factors_rel_of_associated — Mathlib

English

If a is associated to b, then their factor multisets are related by Associated.

Русский

Если a ассоциировано с b, то их множества факторов относятся как ассоциированные.

LaTeX

$$$\mathrm{Associated}(a,b) \Rightarrow \mathrm{Multiset.Rel}(Associated, \mathrm{factors}(a), \mathrm{factors}(b)).$$$

Lean4

theorem factors_rel_of_associated {a b : α} (h : Associated a b) : Multiset.Rel Associated (factors a) (factors b) :=
  by
  rcases iff_iff_and_or_not_and_not.mp h.eq_zero_iff with (⟨rfl, rfl⟩ | ⟨ha, hb⟩)
  · simp
  · refine factors_unique irreducible_of_factor irreducible_of_factor ?_
    exact ((factors_prod ha).trans h).trans (factors_prod hb).symm

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