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.