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
- Int.inductionOn' z b zero succ pred = cast ⋯ (match z - b with | Int.ofNat n => Int.inductionOn'.pos b zero succ n | Int.negSucc n => Int.inductionOn'.neg b zero pred n)
Instances For
The positive case of Int.inductionOn'
.
Equations
- Int.inductionOn'.pos b zero succ 0 = cast ⋯ zero
- Int.inductionOn'.pos b zero succ n.succ = cast ⋯ (succ (b + ↑n) ⋯ (Int.inductionOn'.pos b zero succ n))
Instances For
The negative case of Int.inductionOn'
.
Equations
- Int.inductionOn'.neg b zero pred 0 = pred b ⋯ zero
- Int.inductionOn'.neg b zero pred n.succ = cast ⋯ (pred (b + Int.negSucc n) ⋯ (Int.inductionOn'.neg b zero pred n))
Instances For
Inductively define a function on ℤ
by defining it on ℕ
and extending it from n
to -n
.
Equations
- Int.negInduction nat neg (Int.ofNat n) = nat n
- Int.negInduction nat neg (Int.negSucc n) = neg nat (n + 1)
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
- One or more equations did not get rendered due to their size.
Instances For
mul #
natAbs #
/
#
mod #
properties of /
and %
#
dvd #
/
and ordering #
sign #
toNat #
Alias of Int.toNat_lt_of_ne_zero
.
For use in Mathlib/Tactic/NormNum/Pow.lean