Order instances on the integers

This file contains:

• instances on ℤ. The stronger one is Int.linearOrderedCommRing.
• basic lemmas about integers that involve order properties.

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.linearOrderedCommRing : LinearOrderedCommRing ℤ

Equations

• Int.linearOrderedCommRing = let __src := Int.instCommRingInt; let __src_1 := Int.instLinearOrderInt; let __src_2 := Int.instNontrivialInt; LinearOrderedCommRing.mk ⋯

Extra instances to short-circuit type class resolution

instance Int.orderedCommRing : OrderedCommRing ℤ

Equations

• Int.orderedCommRing = StrictOrderedCommRing.toOrderedCommRing'

instance Int.orderedRing : OrderedRing ℤ

Equations

• Int.orderedRing = StrictOrderedRing.toOrderedRing'

instance Int.linearOrderedAddCommGroup : LinearOrderedAddCommGroup ℤ

Equations

• Int.linearOrderedAddCommGroup = inferInstance

theorem Int.abs_eq_natAbs (a : ℤ) : |a| = ↑(Int.natAbs a)

@[simp]

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

theorem Nat.cast_natAbs {α : Type u_1} [AddGroupWithOne α] (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_sq (x : ℤ) : ↑(Int.natAbs x) ^ 2 = x ^ 2

theorem Int.natAbs_pow_two (x : ℤ) : ↑(Int.natAbs x) ^ 2 = x ^ 2

Alias of Int.natAbs_sq.

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.coe_nat_eq_zero {n : ℕ} : ↑n = 0 ↔ n = 0

theorem Int.coe_nat_ne_zero {n : ℕ} : ↑n ≠ 0 ↔ n ≠ 0

theorem Int.coe_nat_ne_zero_iff_pos {n : ℕ} : ↑n ≠ 0 ↔ 0 < n

theorem Int.abs_coe_nat (n : ℕ) : |↑n| = ↑n

theorem Int.sign_add_eq_of_sign_eq {m : ℤ} {n : ℤ} : Int.sign m = Int.sign n → Int.sign (m + n) = Int.sign n

theorem Int.cast_mul_eq_zsmul_cast {α : Type u_1} [AddCommGroupWithOne α] (m : ℤ) (n : ℤ) : ↑(m * n) = m • ↑n

Note this holds in marginally more generality than Int.cast_mul

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|

theorem Int.emod_two_eq_zero_or_one (n : ℤ) : n % 2 = 0 ∨ n % 2 = 1

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.exists_lt_and_lt_iff_not_dvd (m : ℤ) {n : ℤ} (hn : 0 < n) : (∃ (k : ℤ), n * k < m ∧ m < n * (k + 1)) ↔ ¬n ∣ m

If n > 0 then m is not divisible by n iff it is between n * k and n * (k + 1) for some k.

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.coe_nat_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

theorem bit0_mul {R : Type u_1} [NonUnitalNonAssocRing R] (n : R) (r : R) : bit0 n * r = 2 • (n * r)

theorem mul_bit0 {R : Type u_1} [NonUnitalNonAssocRing R] (n : R) (r : R) : r * bit0 n = 2 • (r * n)

theorem bit1_mul {R : Type u_1} [NonAssocRing R] (n : R) (r : R) : bit1 n * r = 2 • (n * r) + r

theorem mul_bit1 {R : Type u_1} [NonAssocRing R] {n : R} {r : R} : r * bit1 n = 2 • (r * n) + r