English
Let M be a Monoid and p ∈ M with p not a unit. Then either p is irreducible, or p can be written as a product p = a·b with a and b not units.
Русский
Пусть M — моноид и p ∈ M не является единицей. Тогда либо p неразложим, либо p может быть представлено как произведение p = a·b, где a и b не являются единицами.
LaTeX
$$$\\\\forall {M} [Monoid M] \\\\ {p : M}, \\\\neg IsUnit p \\\\Rightarrow \\\\operatorname{Irreducible} p \\\\lor \\\\exists a b \in M, \\\\neg IsUnit a \\\\land \\\\neg IsUnit b \\\\land p = a b$$$
Lean4
@[to_additive]
theorem irreducible_or_factor (hp : ¬IsUnit p) : Irreducible p ∨ ∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ p = a * b := by
simpa [irreducible_iff, hp, and_rotate] using em (∀ a b, p = a * b → IsUnit a ∨ IsUnit b)
