Basic operations on the integers #
This file contains some basic lemmas about integers.
See note [foundational algebra order theory].
This file should not depend on anything defined in Mathlib (except for notation), so that it can be upstreamed to Batteries easily.
Alias of Int.neg_nonpos_iff
.
succ and pred #
Induction on integers: prove a proposition p i
by proving the base case p 0
,
the upwards induction step p i → p (i + 1)
and the downwards induction step p (-i) → p (-i - 1)
.
It is used as the default induction principle for the induction
tactic.
Inductively define a function on ℤ
by defining it at b
, for the succ
of a number greater
than b
, and the pred
of a number less than b
.
Equations
Instances For
A strong recursor for Int
that specifies explicit values for integers below a threshold,
and is analogous to Nat.strongRec
for integers on or above the threshold.
Equations
Instances For
mul #
natAbs #
/
#
mod #
properties of /
and %
#
dvd #
/
and ordering #
sign #
toNat #
The modulus of an integer by another as a natural. Uses the E-rounding convention.
Equations
Instances For
For use in Mathlib/Tactic/NormNum/Pow.lean