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.

instance Int.linearOrderedAddCommGroup : LinearOrderedAddCommGroup ℤ

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

succ and pred

theorem Int.lt_succ_self (a : ℤ) : a < a.succ

theorem Int.pred_self_lt (a : ℤ) : a.pred < a

theorem Int.le_add_one_iff {m : ℤ} {n : ℤ} : m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1

theorem Int.sub_one_lt_iff {a : ℤ} {b : ℤ} : a - 1 < b ↔ a ≤ b

theorem Int.le_sub_one_iff {a : ℤ} {b : ℤ} : a ≤ b - 1 ↔ a < b

@[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|

def Int.inductionOn' {C : ℤ → Sort u_1} (z : ℤ) (b : ℤ) (H0 : C b) (Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)) (Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)) : C z

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

• z.inductionOn' b H0 Hs Hp = ⋯.mpr (⋯.mpr (match z - b with | Int.ofNat n => Int.inductionOn'.pos b H0 Hs n | Int.negSucc n => Int.inductionOn'.neg b H0 Hp n))

def Int.inductionOn'.pos {C : ℤ → Sort u_1} (b : ℤ) (H0 : C b) (Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)) (n : ℕ) : C (b + ↑n)

The positive case of Int.inductionOn'.

Equations

• Int.inductionOn'.pos b H0 Hs 0 = cast ⋯ H0
• Int.inductionOn'.pos b H0 Hs n.succ = cast ⋯ (Hs (b + ↑n) ⋯ (Int.inductionOn'.pos b H0 Hs n))

def Int.inductionOn'.neg {C : ℤ → Sort u_1} (b : ℤ) (H0 : C b) (Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)) (n : ℕ) : C (b + Int.negSucc n)

The negative case of Int.inductionOn'.

Equations

• Int.inductionOn'.neg b H0 Hp 0 = Hp b ⋯ H0
• Int.inductionOn'.neg b H0 Hp n.succ = cast ⋯ (Hp (b + Int.negSucc n) ⋯ (Int.inductionOn'.neg b H0 Hp n))

theorem Int.le_induction {P : ℤ → Prop} {m : ℤ} (h0 : P m) (h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)) (n : ℤ) : m ≤ n → P n

See Int.inductionOn' for an induction in both directions.

theorem Int.le_induction_down {P : ℤ → Prop} {m : ℤ} (h0 : P m) (h1 : ∀ (n : ℤ), n ≤ m → P n → P (n - 1)) (n : ℤ) : n ≤ m → P n

See Int.inductionOn' for an induction in both directions.

nat abs

/

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|

theorem Int.add_emod_eq_add_mod_right {m : ℤ} {n : ℤ} {k : ℤ} (i : ℤ) (H : m % n = k % n) : (m + i) % n = (k + i) % n

@[simp]

theorem Int.neg_emod_two (i : ℤ) : -i % 2 = i % 2

properties of / and %

theorem Int.abs_ediv_le_abs (a : ℤ) (b : ℤ) : |a / b| ≤ |a|

dvd

theorem Int.ediv_dvd_ediv {a : ℤ} {b : ℤ} {c : ℤ} : a ∣ b → b ∣ c → b / a ∣ c / 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|

/ and ordering

theorem Int.natAbs_eq_of_dvd_dvd {s : ℤ} {t : ℤ} (hst : s ∣ t) (hts : t ∣ s) : s.natAbs = t.natAbs

theorem Int.ediv_dvd_of_dvd {s : ℤ} {t : ℤ} (hst : s ∣ t) : t / s ∣ t

toNat

@[simp]

theorem Int.toNat_le {a : ℤ} {n : ℕ} : a.toNat ≤ n ↔ a ≤ ↑n

@[simp]

theorem Int.lt_toNat {n : ℕ} {a : ℤ} : n < a.toNat ↔ ↑n < a

@[simp]

theorem Int.natCast_nonpos_iff {n : ℕ} : ↑n ≤ 0 ↔ n = 0

theorem Int.toNat_le_toNat {a : ℤ} {b : ℤ} (h : a ≤ b) : a.toNat ≤ b.toNat

theorem Int.toNat_lt_toNat {a : ℤ} {b : ℤ} (hb : 0 < b) : a.toNat < b.toNat ↔ a < b

theorem Int.lt_of_toNat_lt {a : ℤ} {b : ℤ} (h : a.toNat < b.toNat) : a < b

@[simp]

theorem Int.toNat_pred_coe_of_pos {i : ℤ} (h : 0 < i) : ↑(i.toNat - 1) = i - 1

@[simp]

theorem Int.toNat_eq_zero {n : ℤ} : n.toNat = 0 ↔ n ≤ 0

@[simp]

theorem Int.toNat_sub_of_le {a : ℤ} {b : ℤ} (h : b ≤ a) : ↑(a - b).toNat = a - b

@[simp]

theorem abs_zsmul_eq_zero {G : Type u_1} [AddGroup G] (a : G) (n : ℤ) : |n| • a = 0 ↔ n • a = 0

@[simp]

theorem zpow_abs_eq_one {G : Type u_1} [Group G] (a : G) (n : ℤ) : a ^ |n| = 1 ↔ a ^ n = 1