# 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 only Prop-valued.
• Int.inductionOn': Simple growing induction for numbers greater than b, plus simple decreasing induction on numbers less than b.
theorem Int.natCast_strictMono :
StrictMono fun (x : ) => x
@[deprecated Int.natCast_strictMono]
theorem Int.coe_nat_strictMono :
StrictMono fun (x : ) => x

Alias of Int.natCast_strictMono.

Equations
• One or more equations did not get rendered due to their size.

### Miscellaneous lemmas #

theorem Int.abs_eq_natAbs (a : ) :
|a| = a.natAbs
@[simp]
theorem Int.natCast_natAbs (n : ) :
n.natAbs = |n|
theorem Int.natAbs_abs (a : ) :
|a|.natAbs = a.natAbs
theorem Int.sign_mul_abs (a : ) :
a.sign * |a| = a
theorem Int.natAbs_le_self_sq (a : ) :
a.natAbs a ^ 2
theorem Int.natAbs_le_self_pow_two (a : ) :
a.natAbs a ^ 2

Alias of Int.natAbs_le_self_sq.

theorem Int.le_self_sq (b : ) :
b b ^ 2
theorem Int.le_self_pow_two (b : ) :
b b ^ 2

Alias of Int.le_self_sq.

theorem Int.abs_natCast (n : ) :
|n| = n
theorem Int.natAbs_sub_pos_iff {i : } {j : } :
0 < (i - j).natAbs i j
theorem Int.natAbs_sub_ne_zero_iff {i : } {j : } :
(i - j).natAbs 0 i j
@[simp]
theorem Int.abs_lt_one_iff {a : } :
|a| < 1 a = 0
theorem Int.abs_le_one_iff {a : } :
|a| 1 a = 0 a = 1 a = -1
theorem Int.one_le_abs {z : } (h₀ : z 0) :
1 |z|

#### /#

theorem Int.ediv_eq_zero_of_lt_abs {a : } {b : } (H1 : 0 a) (H2 : a < |b|) :
a / b = 0

#### mod #

@[simp]
theorem Int.emod_abs (a : ) (b : ) :
a % |b| = a % b
theorem Int.emod_lt (a : ) {b : } (H : b 0) :
a % b < |b|

### properties of / and %#

theorem Int.abs_ediv_le_abs (a : ) (b : ) :
|a / b| |a|
theorem Int.abs_sign_of_nonzero {z : } (hz : z 0) :
|z.sign| = 1
theorem Int.sign_eq_ediv_abs (a : ) :
a.sign = a / |a|
@[simp]
theorem abs_zsmul_eq_zero {G : Type u_1} [] (a : G) (n : ) :
|n| a = 0 n a = 0
@[simp]
theorem zpow_abs_eq_one {G : Type u_1} [] (a : G) (n : ) :
a ^ |n| = 1 a ^ n = 1