English
Let a be an element of a commutative monoid with zero that is well-founded with respect to irreducible divisors. If a is not a unit and a ≠ 0, then there exists an irreducible element i with i ∣ a.
Русский
Пусть a — элемент коммутативного моноида с нулём, где существует делимость по ирредуцируемым; если a не является единицей и a ≠ 0, то существует ирредуцируемый элемент i, такой что i делит a.
LaTeX
$$$\forall a\in\alpha,\ a \neq 0 \land \lnot\mathrm{IsUnit}(a) \Rightarrow \exists i,\mathrm{Irreducible}(i) \land i \mid a.$$$
Lean4
theorem exists_irreducible_factor {a : α} (ha : ¬IsUnit a) (ha0 : a ≠ 0) : ∃ i, Irreducible i ∧ i ∣ a :=
let ⟨b, hs, hr⟩ := wellFounded_dvdNotUnit.has_min {b | b ∣ a ∧ ¬IsUnit b} ⟨a, dvd_rfl, ha⟩
⟨b,
⟨hs.2, fun c d he =>
let h := dvd_trans ⟨d, he⟩ hs.1
or_iff_not_imp_left.2 fun hc => of_not_not fun hd => hr c ⟨h, hc⟩ ⟨ne_zero_of_dvd_ne_zero ha0 h, d, hd, he⟩⟩,
hs.1⟩
