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 (_ : ∀ (a b : ℤ), a * b = b * a)

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

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

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

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 (_ : C b = C (b + ↑0)) H0
• Int.inductionOn'.pos b H0 Hs (Nat.succ n) = cast (_ : C (b + ↑n + 1) = C (b + ↑(n + 1))) (Hs (b + ↑n) (_ : b ≤ 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

• One or more equations did not get rendered due to their size.
• Int.inductionOn'.neg b H0 Hp 0 = Hp b (_ : b ≤ b) H0

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.ediv_mul_le (a : ℤ) {b : ℤ} (H : b ≠ 0) : a / b * b ≤ a

theorem Int.ediv_le_of_le_mul {a : ℤ} {b : ℤ} {c : ℤ} (H : 0 < c) (H' : a ≤ b * c) : a / c ≤ b

theorem Int.mul_lt_of_lt_ediv {a : ℤ} {b : ℤ} {c : ℤ} (H : 0 < c) (H3 : a < b / c) : a * c < b

theorem Int.mul_le_of_le_ediv {a : ℤ} {b : ℤ} {c : ℤ} (H1 : 0 < c) (H2 : a ≤ b / c) : a * c ≤ b

theorem Int.le_ediv_of_mul_le {a : ℤ} {b : ℤ} {c : ℤ} (H1 : 0 < c) (H2 : a * c ≤ b) : a ≤ b / c

theorem Int.le_ediv_iff_mul_le {a : ℤ} {b : ℤ} {c : ℤ} (H : 0 < c) : a ≤ b / c ↔ a * c ≤ b

theorem Int.ediv_le_ediv {a : ℤ} {b : ℤ} {c : ℤ} (H : 0 < c) (H' : a ≤ b) : a / c ≤ b / c

theorem Int.ediv_lt_of_lt_mul {a : ℤ} {b : ℤ} {c : ℤ} (H : 0 < c) (H' : a < b * c) : a / c < b

theorem Int.lt_mul_of_ediv_lt {a : ℤ} {b : ℤ} {c : ℤ} (H1 : 0 < c) (H2 : a / c < b) : a < b * c

theorem Int.ediv_lt_iff_lt_mul {a : ℤ} {b : ℤ} {c : ℤ} (H : 0 < c) : a / c < b ↔ a < b * c

theorem Int.le_mul_of_ediv_le {a : ℤ} {b : ℤ} {c : ℤ} (H1 : 0 ≤ b) (H2 : b ∣ a) (H3 : a / b ≤ c) : a ≤ c * b

theorem Int.lt_ediv_of_mul_lt {a : ℤ} {b : ℤ} {c : ℤ} (H1 : 0 ≤ b) (H2 : b ∣ c) (H3 : a * b < c) : a < c / b

theorem Int.lt_ediv_iff_mul_lt {a : ℤ} {b : ℤ} (c : ℤ) (H : 0 < c) (H' : c ∣ b) : a < b / c ↔ a * c < b

theorem Int.ediv_pos_of_pos_of_dvd {a : ℤ} {b : ℤ} (H1 : 0 < a) (H2 : 0 ≤ b) (H3 : b ∣ a) : 0 < a / b

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

theorem Int.ediv_eq_ediv_of_mul_eq_mul {a : ℤ} {b : ℤ} {c : ℤ} {d : ℤ} (H2 : d ∣ c) (H3 : b ≠ 0) (H4 : d ≠ 0) (H5 : a * d = b * c) : a / b = c / d

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

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