Commit 2021-09-07 21:34 b0b0a24f
View on Github →feat(data/int): absolute values and integers (#9028)
We prove that an absolute value maps all units ℤ
to 1
.
I added a new file since there is no neat place in the import hierarchy where this fit (the meet of algebra.algebra.basic
and data.int.cast
).