Negative_of_Division_Product_v2
Proveddivisionproofwikirings
Let R be a commutative ring with unity. Then -(x/z) = (-x)/z = x/(-z).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Negative_of_Division_Product_v2 {F : Type _} [Field F] (x z : F) (hz : z ≠ 0) : -(x / z) = (-x) / z := by sorrySource