Basic operations on the integers #
This file contains:
- instances on
ℤ
. The stronger one isInt.linearOrderedCommRing
. - some basic lemmas about integers
@[simp]
Extra instances to short-circuit type class resolution #
These also prevent non-computable instances like Int.normedCommRing
being used to construct
these instances non-computably.
succ and pred #
nat abs #
@[deprecated Int.natAbs_ne_zero]