Ring_Less_Zero_is_Semigroup_for_Product_iff_No_Proper_Zero_Divisors
Provedproofwikiringssemigroupszero-divisors
Let (R, +, ) be a non-null ring. Then R has no zero divisors iff (R, *) is a semigroup.
Preamble
import Mathlib.Algebra.Ring.Basic
Formal statement
theorem Ring_Less_Zero_is_Semigroup_for_Product_iff_No_Proper_Zero_Divisors {R : Type _} [Ring R] [Nontrivial R] : NoZeroDivisors R ↔ ∀ a b : R, a ≠ 0 → b ≠ 0 → a * b ≠ 0 := by sorrySource