English
In CancelCommMonoidWithZero M, for x,y in M, Prime(x*y) holds iff either x is prime and y is a unit, or x is a unit and y is prime.
Русский
В CancelCommMonoidWithZero M для x,y в M: Prime(x*y) равно истинности либо (Prime x и IsUnit y) либо (IsUnit x и Prime y).
LaTeX
$$$ [CancelCommMonoidWithZero M] {x y : M}, Prime (x * y) \iff (Prime x \land IsUnit y) \lor (IsUnit x \land Prime y) $$$
Lean4
theorem prime_mul_iff [CancelCommMonoidWithZero M] {x y : M} :
Prime (x * y) ↔ (Prime x ∧ IsUnit y) ∨ (IsUnit x ∧ Prime y) :=
by
refine ⟨fun h ↦ ?_, ?_⟩
· rcases of_irreducible_mul h.irreducible with hx | hy
· exact Or.inr ⟨hx, (associated_unit_mul_left y x hx).prime h⟩
· exact Or.inl ⟨(associated_mul_unit_left x y hy).prime h, hy⟩
· rintro (⟨hx, hy⟩ | ⟨hx, hy⟩)
· exact (associated_mul_unit_left x y hy).symm.prime hx
· exact (associated_unit_mul_right y x hx).prime hy
