Mathlib v3 is deprecated. Go to Mathlib v4

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).

Estimated changes