Commit 2025-04-24 20:38 fd19b25b

View on Github →

chore(Ring/Basic): merge inv_neg and inv_neg' (#24335) The non-primed version was strictly more general. Also rename instHasDistribNeg to MulOpposite.instHasDistribNeg.

Estimated changes

Modified Mathlib/Algebra/Order/Field/Power.lean

Modified Mathlib/Algebra/Ring/Basic.lean

deleted theorem inv_neg'

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

Modified Mathlib/LinearAlgebra/Orientation.lean