mathlib

3f26dfe2 - feat(data/int/basic): Units are either equal or negatives of each other (#14517)

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.