English
In a monoid, Irreducible (x·y) holds exactly when either x is irreducible and y is a unit, or y is irreducible and x is a unit.
Русский
В моноиде Irreducible (x·y) выполняется тогда, когда либо x неразложим и y единица, либо y неразложим и x единица.
LaTeX
$$$\\\\forall {M} [Monoid M] {x y : M}, \\\\Irreducible (x y) \\\\Leftrightarrow \\\\big( (\\\\Irreducible x \\\\land \\\\IsUnit y) \\\\lor \\\\big( \\\\Irreducible y \\\\land \\\\IsUnit x) \\\\big)$$$
Lean4
@[to_additive]
theorem irreducible_mul_iff : Irreducible (x * y) ↔ Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x :=
by
constructor
· refine fun h => Or.imp (fun h' => ⟨?_, h'⟩) (fun h' => ⟨?_, h'⟩) (h.isUnit_or_isUnit rfl).symm
· rwa [irreducible_mul_isUnit h'] at h
· rwa [irreducible_isUnit_mul h'] at h
· rintro (⟨ha, hb⟩ | ⟨hb, ha⟩)
· rwa [irreducible_mul_isUnit hb]
· rwa [irreducible_isUnit_mul ha]
