English
Under suitable hypotheses, an element is irreducible if and only if it is prime.
Русский
При разумных предпосылках неразложимый элемент эквивалентен простому элементу.
LaTeX
$$$\forall p:\, \alpha,\; \mathrm{Irreducible}(p) \iff \mathrm{Prime}(p).$$$
Lean4
theorem irreducible_iff_prime_of_existsUnique_irreducible_factors [CancelCommMonoidWithZero α]
(eif : ∀ a : α, a ≠ 0 → ∃ f : Multiset α, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a)
(uif :
∀ f g : Multiset α,
(∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g)
(p : α) : Irreducible p ↔ Prime p :=
letI := Classical.decEq α
⟨fun hpi =>
⟨hpi.ne_zero, hpi.1, fun a b ⟨x, hx⟩ =>
if hab0 : a * b = 0 then
(eq_zero_or_eq_zero_of_mul_eq_zero hab0).elim (fun ha0 => by simp [ha0]) fun hb0 => by simp [hb0]
else by
have hx0 : x ≠ 0 := fun hx0 => by simp_all
have ha0 : a ≠ 0 := left_ne_zero_of_mul hab0
have hb0 : b ≠ 0 := right_ne_zero_of_mul hab0
obtain ⟨fx, hfx⟩ := eif x hx0
obtain ⟨fa, hfa⟩ := eif a ha0
obtain ⟨fb, hfb⟩ := eif b hb0
have h : Multiset.Rel Associated (p ::ₘ fx) (fa + fb) :=
by
apply uif
· exact fun i hi => (Multiset.mem_cons.1 hi).elim (fun hip => hip.symm ▸ hpi) (hfx.1 _)
· exact fun i hi => (Multiset.mem_add.1 hi).elim (hfa.1 _) (hfb.1 _)
calc
Multiset.prod (p ::ₘ fx) ~ᵤ a * b := by rw [hx, Multiset.prod_cons]; exact hfx.2.mul_left _
_ ~ᵤ fa.prod * fb.prod := (hfa.2.symm.mul_mul hfb.2.symm)
_ = _ := by rw [Multiset.prod_add]
exact
let ⟨q, hqf, hq⟩ := Multiset.exists_mem_of_rel_of_mem h (Multiset.mem_cons_self p _)
(Multiset.mem_add.1 hqf).elim
(fun hqa => Or.inl <| hq.dvd_iff_dvd_left.2 <| hfa.2.dvd_iff_dvd_right.1 (Multiset.dvd_prod hqa)) fun hqb =>
Or.inr <| hq.dvd_iff_dvd_left.2 <| hfb.2.dvd_iff_dvd_right.1 (Multiset.dvd_prod hqb)⟩,
Prime.irreducible⟩
