The integers form a linear ordered group #
This file contains the linear ordered group instance on the integers.
See note [foundational algebra order theory].
Recursors #
Int.rec
: Sign disjunction. Something is true/defined onℤ
if it's true/defined for nonnegative and for negative values. (Defined in core Lean 3)Int.inductionOn
: Simple growing induction on positive numbers, plus simple decreasing induction on negative numbers. Note that this recursor is currently onlyProp
-valued.Int.inductionOn'
: Simple growing induction for numbers greater thanb
, plus simple decreasing induction on numbers less thanb
.
@[deprecated Int.natCast_strictMono]
Alias of Int.natCast_strictMono
.
Equations
- One or more equations did not get rendered due to their size.