Ring_Element_is_Zero_Divisor_iff_not_Cancellable
Provedproofwikiringszero-divisors
Let (R, +, ) be a non-null ring. Let z ∈ R. Then z is a zero divisor iff z is not cancellable.
Preamble
import Mathlib.Algebra.Ring.Basic
Formal statement
theorem Ring_Element_is_Zero_Divisor_iff_not_Cancellable {R : Type _} [Ring R] [Nontrivial R] (z : R) (hz : z ≠ 0) : (∃ w : R, w ≠ 0 ∧ z * w = 0) ↔ ¬(∀ a b : R, z * a = z * b → a = b) := by sorrySource