Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-04 13:17 3f26dfe2

View on Github →

feat(data/int/basic): Units are either equal or negatives of each other (#14517) This PR adds a lemma stating that units in the integers are either equal or negatives of each other. I have found this lemma to be useful for casework.

Estimated changes