factors'_cong — Mathlib

English

If a is associated to b, then their factors' multisets are equal.

Русский

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

LaTeX

$$h : a ~ᵤ b → factors' a = factors' b$$

Lean4

theorem factors'_cong {a b : α} (h : a ~ᵤ b) : factors' a = factors' b :=
  by
  obtain rfl | hb := eq_or_ne b 0
  · rw [associated_zero_iff_eq_zero] at h
    rw [h]
  have ha : a ≠ 0 := by
    contrapose! hb with ha
    rw [← associated_zero_iff_eq_zero, ← ha]
    exact h.symm
  rw [← Multiset.map_eq_map Subtype.coe_injective, map_subtype_coe_factors', map_subtype_coe_factors', ←
    rel_associated_iff_map_eq_map]
  exact
    factors_unique irreducible_of_factor irreducible_of_factor
      ((factors_prod ha).trans <| h.trans <| (factors_prod hb).symm)

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