Revision #2617 → #3904 · back to history
modifiedUnary negation of positive6e715caedcfc
| Field | From #2617 | To #3904 |
|---|
| mathlib.module | Mathlib.Algebra.Order.Group.Unbundled.Basic | Mathlib.Algebra.Order.Group.Defs |
| note | `neg_pos`/`neg_neg_of_pos` express that negating a positive number yields a negative number. | `neg_neg_of_pos : 0 < a → -a < 0` expresses that negating a positive number yields a negative number. |
addedDistributive law forces (−)(−)=+02016b9e1e0a
addedSum of a number and its negation is zerobf6964d8b66c
modifiedTotal order on integers41951d3c3e8c
| Field | From #2617 | To #3904 |
|---|
| mathlib.module | Mathlib.Data.Int.Order | Mathlib.Data.Int.Order.Basic |
addedGrothendieck construction137ebeef837e
addedCancellation law for additionb5a3abc17bea