English
Repeated assertion: well-foundedness on associates is equivalent to well-foundedness of the lt relation.
Русский
Повторное утверждение: хорошо упорядоченность на ассоциированных эквивалентна хорошо упорядоченности отношения lt.
LaTeX
$$theorem wellFoundedLT_associates$$
Lean4
theorem prime_factors_unique [CancelCommMonoidWithZero α] :
∀ {f g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g := by
classical
intro f
induction f using Multiset.induction_on with
| empty =>
intro g _ hg h
exact
Multiset.rel_zero_left.2 <|
Multiset.eq_zero_of_forall_notMem fun x hx =>
have : IsUnit g.prod := by simpa [associated_one_iff_isUnit] using h.symm
(hg x hx).not_unit <| isUnit_iff_dvd_one.2 <| (Multiset.dvd_prod hx).trans (isUnit_iff_dvd_one.1 this)
| cons p f ih =>
intro g hf hg hfg
let ⟨b, hbg, hb⟩ :=
(exists_associated_mem_of_dvd_prod (hf p (by simp)) fun q hq => hg _ hq) <|
hfg.dvd_iff_dvd_right.1 (show p ∣ (p ::ₘ f).prod by simp)
haveI := Classical.decEq α
rw [← Multiset.cons_erase hbg]
exact
Multiset.Rel.cons hb
(ih (fun q hq => hf _ (by simp [hq])) (fun {q} (hq : q ∈ g.erase b) => hg q (Multiset.mem_of_mem_erase hq))
(Associated.of_mul_left (by rwa [← Multiset.prod_cons, ← Multiset.prod_cons, Multiset.cons_erase hbg]) hb
(hf p (by simp)).ne_zero))
