Product_is_Zero_Divisor_means_Zero_Divisor
Provedproofwikiringszero-divisors
If the ring product of two elements of a ring is a zero divisor, then one of the two elements must be a zero divisor.
Preamble
import Mathlib.Algebra.Ring.Basic
Formal statement
theorem Product_is_Zero_Divisor_means_Zero_Divisor {R : Type _} [Ring R] (x y : R) (hx : x ≠ 0) (hy : y ≠ 0) (h : ∃ z : R, z ≠ 0 ∧ (x * y) * z = 0) : (∃ w : R, w ≠ 0 ∧ x * w = 0) ∨ (∃ w : R, w ≠ 0 ∧ y * w = 0) := by sorrySource