Product_of_Negative_with_Product_Inverse_v2
Provedproofwikiringsunits
Let R be a ring with unity. Let z be a unit. Then -(x * z⁻¹) = (-x) * z⁻¹.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Product_of_Negative_with_Product_Inverse_v2 {F : Type _} [Field F] (x z : F) (hz : z ≠ 0) : -(x * z⁻¹) = (-x) * z⁻¹ := by sorrySource