Theorem Left.neg_of_mul_neg_right

Modification history

2024-07-25 07:50

Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

chore(Algebra/Order/GroupWithZero/Unbundled): resolving name inconsistencies (#9904) …

Modified Left.neg_of_mul_neg_right View on Github →

2022-11-23 19:15

Mathlib/Algebra/Order/Ring/Lemmas.lean

feat: port Algebra.Order.Ring.Lemmas (#482) …

Added Left.neg_of_mul_neg_right View on Github →