English
If an irreducible element a has a prime factorization f, then a is associate to one of the prime factors in f, and f must be the singleton consisting of that prime.
Русский
Если ирредуцируемый элемент a имеет разложение на простые факторизмы f, то a ассоциирован с одним из простых факторов в f, и f состоит ровно из этого единственного простого.
LaTeX
$$$\forall a\,\big(\mathrm{Irreducible}(a)\land (\exists f:\\mathrm{Multiset}(\alpha), (\forall b\in f, \mathrm{Prime}(b)) \land f.prod \sim_u a)\big) \Rightarrow \exists p\in f:\; a \sim p \\land f = \{p\}.$$$
Lean4
/-- If an irreducible has a prime factorization,
then it is an associate of one of its prime factors. -/
theorem prime_factors_irreducible [CommMonoidWithZero α] {a : α} {f : Multiset α} (ha : Irreducible a)
(pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a) : ∃ p, a ~ᵤ p ∧ f = { p } :=
by
haveI := Classical.decEq α
refine
@Multiset.induction_on _ (fun g => (g.prod ~ᵤ a) → (∀ b ∈ g, Prime b) → ∃ p, a ~ᵤ p ∧ g = { p }) f ?_ ?_ pfa.2 pfa.1
· intro h; exact (ha.not_isUnit (associated_one_iff_isUnit.1 (Associated.symm h))).elim
· rintro p s _ ⟨u, hu⟩ hs
use p
have hs0 : s = 0 := by
by_contra hs0
obtain ⟨q, hq⟩ := Multiset.exists_mem_of_ne_zero hs0
apply (hs q (by simp [hq])).2.1
refine (ha.isUnit_or_isUnit (?_ : _ = p * ↑u * (s.erase q).prod * _)).resolve_left ?_
· rw [mul_right_comm _ _ q, mul_assoc, ← Multiset.prod_cons, Multiset.cons_erase hq, ← hu, mul_comm, mul_comm p _,
mul_assoc]
simp
apply mt isUnit_of_mul_isUnit_left (mt isUnit_of_mul_isUnit_left _)
apply (hs p (Multiset.mem_cons_self _ _)).2.1
simp only [mul_one, Multiset.prod_cons, Multiset.prod_zero, hs0] at *
exact ⟨Associated.symm ⟨u, hu⟩, rfl⟩
