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