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