ℤ with the ordering. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
If an integer with larger absolute value divides an integer, it is
If two integers are congruent to a sufficiently large modulus,
they are equal.