English
For a nonzero not-unit element a in a WfDvdMonoid, a is not a unit if and only if there exists a multiset f of irreducibles with f.prod = a and f ≠ ∅.
Русский
Для не нулевого неединичного элемента a в WfDvdMonoid неверно единица тогда и только тогда, когда существует мультисет f ирредуцируемых, таких что произведение f равно a и f не пуст.
LaTeX
$$$\forall a \ (a \neq 0) \Rightarrow (\lnot \mathrm{IsUnit}(a) \iff \exists f : \mathrm{Multiset}\ \alpha,\ (\forall b \in f, \mathrm{Irreducible}(b)) \land (f.prod = a) \land f \neq \emptyset).$$$
Lean4
theorem not_unit_iff_exists_factors_eq (a : α) (hn0 : a ≠ 0) :
¬IsUnit a ↔ ∃ f : Multiset α, (∀ b ∈ f, Irreducible b) ∧ f.prod = a ∧ f ≠ ∅ :=
⟨fun hnu => by
obtain ⟨f, hi, u, rfl⟩ := exists_factors a hn0
obtain ⟨b, h⟩ := Multiset.exists_mem_of_ne_zero fun h : f = 0 => hnu <| by simp [h]
classical
refine ⟨(f.erase b).cons (b * u), fun a ha => ?_, ?_, Multiset.cons_ne_zero⟩
· obtain rfl | ha := Multiset.mem_cons.1 ha
exacts [Associated.irreducible ⟨u, rfl⟩ (hi b h), hi a (Multiset.mem_of_mem_erase ha)]
· rw [Multiset.prod_cons, mul_comm b, mul_assoc, Multiset.prod_erase h, mul_comm],
fun ⟨_, hi, he, hne⟩ =>
let ⟨b, h⟩ := Multiset.exists_mem_of_ne_zero hne
not_isUnit_of_not_isUnit_dvd (hi b h).not_isUnit <| he ▸ Multiset.dvd_prod h⟩
