English
In a nontrivial Unique Factorization Monoid, if two factor sets have the same product, then they are equal.
Русский
В неприводимом уникальном факторизационном моноиде, если два набора факторов имеют один и тот же произведение, то они равны.
LaTeX
$$p.prod = q.prod → p = q$$
Lean4
theorem unique [Nontrivial α] {p q : FactorSet α} (h : p.prod = q.prod) : p = q := by
-- TODO: `induction_eliminator` doesn't work with `abbrev`
unfold FactorSet at p q
induction p <;> induction q
· rfl
· rw [eq_comm, ← FactorSet.prod_eq_zero_iff, ← h, Associates.prod_top]
· rw [← FactorSet.prod_eq_zero_iff, h, Associates.prod_top]
· congr 1
rw [← Multiset.map_eq_map Subtype.coe_injective]
apply unique' _ _ h <;>
· intro a ha
obtain ⟨⟨a', irred⟩, -, rfl⟩ := Multiset.mem_map.mp ha
rwa [Subtype.coe_mk]
