English
If a ≠ 0, b ≠ 0, and for all irreducible p, count p in a.factors equals count p in b.factors, then a.factors = b.factors.
Русский
Если a ≠ 0, b ≠ 0 и для каждого неприводимого p выполняется count p в a.factors = count p в b.factors, то a.factors = b.factors.
LaTeX
$$Ne a 0 → Ne b 0 → (∀ p, Irreducible p → p.count a.factors = p.count b.factors) → a.factors = b.factors$$
Lean4
theorem eq_factors_of_eq_counts {a b : Associates α} (ha : a ≠ 0) (hb : b ≠ 0)
(h : ∀ p : Associates α, Irreducible p → p.count a.factors = p.count b.factors) : a.factors = b.factors :=
by
obtain ⟨sa, h_sa⟩ := factors_eq_some_iff_ne_zero.mpr ha
obtain ⟨sb, h_sb⟩ := factors_eq_some_iff_ne_zero.mpr hb
rw [h_sa, h_sb] at h ⊢
rw [WithTop.coe_eq_coe]
have h_count : ∀ (p : Associates α) (hp : Irreducible p), sa.count ⟨p, hp⟩ = sb.count ⟨p, hp⟩ :=
by
intro p hp
rw [← count_some, ← count_some, h p hp]
apply Multiset.toFinsupp.injective
ext ⟨p, hp⟩
rw [Multiset.toFinsupp_apply, Multiset.toFinsupp_apply, h_count p hp]
