Ring_Product_with_Zero
Provedproofwikiring-product-with-zerorings
Let (R, +, *) be a ring whose zero is 0. Then for all x in R, 0 * x = 0 = x * 0.
Preamble
import Mathlib.Algebra.Ring.Basic
Formal statement
theorem Ring_Product_with_Zero {R : Type _} [Ring R] (x : R) : 0 * x = 0 ∧ x * 0 = 0 := by sorrySource