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| = ↑(Int.natAbs a)

@[simp]

theorem Int.natCast_natAbs (n : ℤ) : ↑(Int.natAbs n) = |n|

theorem Int.natAbs_abs (a : ℤ) : Int.natAbs |a| = Int.natAbs a

theorem Int.sign_mul_abs (a : ℤ) : Int.sign a * |a| = a

theorem Int.natAbs_le_self_sq (a : ℤ) : ↑(Int.natAbs a) ≤ a ^ 2

theorem Int.natAbs_le_self_pow_two (a : ℤ) : ↑(Int.natAbs a) ≤ 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 < Int.natAbs (i - j) ↔ i ≠ j

theorem Int.natAbs_sub_ne_zero_iff {i : ℤ} {j : ℤ} : Int.natAbs (i - j) ≠ 0 ↔ i ≠ j

succ and pred

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

theorem Int.pred_self_lt (a : ℤ) : Int.pred a < 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

• Int.inductionOn' z b H0 Hs Hp = Eq.mpr ⋯ (Eq.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 (Nat.succ n) = 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 (Nat.succ n) = 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) : |Int.sign z| = 1

theorem Int.sign_eq_ediv_abs (a : ℤ) : Int.sign a = a / |a|

/ and ordering

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

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

toNat

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem Int.toNat_sub_of_le {a : ℤ} {b : ℤ} (h : b ≤ a) : ↑(Int.toNat (a - b)) = 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