Product_with_Ring_Negative
Provedproofwikiring-negativesrings
Let (R, +, *) be a ring. Then for all x, y in R, (-x) * y = -(x * y) = x * (-y).
Preamble
import Mathlib.Algebra.Ring.Basic
Formal statement
theorem Product_with_Ring_Negative {R : Type _} [Ring R] (x y : R) : (-x) * y = -(x * y) ∧ x * (-y) = -(x * y) := by sorrySource