mathlib3 documentation

data.int.order.basic

Order instances on the integers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains:

Recursors #

source
@[protected, instance]
def int.linear_ordered_comm_ring  :
linear_ordered_comm_ring ℤ
Equations

Extra instances to short-circuit type class resolution #

source
@[protected, instance]
def int.ordered_comm_ring  :
ordered_comm_ring ℤ
Equations
source
@[protected, instance]
def int.ordered_ring  :
ordered_ring ℤ
Equations
source
@[protected, instance]
def int.linear_ordered_add_comm_group  :
linear_ordered_add_comm_group ℤ
Equations
source
theorem int.abs_eq_nat_abs (a : ℤ) :
|a| = ↑(a.nat_abs)
source
@[simp, norm_cast]
theorem int.coe_nat_abs (n : ℤ) :
↑(n.nat_abs) = |n|
source
theorem nat.cast_nat_abs {α : Type u_1} [add_group_with_one α] (n : ℤ) :
↑(n.nat_abs) = ↑|n|
source
theorem int.nat_abs_abs (a : ℤ) :
|a|.nat_abs = a.nat_abs
source
theorem int.sign_mul_abs (a : ℤ) :
a.sign * |a| = a
source
theorem int.coe_nat_eq_zero {n : ℕ} :
↑n = 0 ↔ n = 0
source
theorem int.coe_nat_ne_zero {n : ℕ} :
↑n ≠ 0 ↔ n ≠ 0
source
theorem int.coe_nat_ne_zero_iff_pos {n : ℕ} :
↑n ≠ 0 ↔ 0 < n
source
@[norm_cast]
theorem int.abs_coe_nat (n : ℕ) :
|↑n| = ↑n
source
theorem int.sign_add_eq_of_sign_eq {m n : ℤ} :
m.sign = n.sign → (m + n).sign = n.sign

succ and pred #

source
theorem int.lt_succ_self (a : ℤ) :
a < a.succ
source
theorem int.pred_self_lt (a : ℤ) :
a.pred < a
source
theorem int.lt_add_one_iff {a b : ℤ} :
a < b + 1 ↔ a ≤ b
source
theorem int.le_add_one {a b : ℤ} (h : a ≤ b) :
a ≤ b + 1
source
theorem int.sub_one_lt_iff {a b : ℤ} :
a - 1 < b ↔ a ≤ b
source
theorem int.le_sub_one_iff {a b : ℤ} :
a ≤ b - 1 ↔ a < b
source
@[simp]
theorem int.abs_lt_one_iff {a : ℤ} :
|a| < 1 ↔ a = 0
source
theorem int.abs_le_one_iff {a : ℤ} :
|a| ≤ 1 ↔ a = 0 ∨ a = 1 ∨ a = -1
source
theorem int.one_le_abs {z : ℤ} (h₀ : z ≠ 0) :
1 ≤ |z|
source
@[protected]
def int.induction_on' {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
source
@[protected]
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.induction_on' for an induction in both directions.

source
@[protected]
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.induction_on' for an induction in both directions.

nat abs #

source
@[simp]
theorem int.nat_abs_dvd_iff_dvd {a b : ℤ} :
a.nat_abs ∣ b.nat_abs ↔ a ∣ b

/ #

source
@[protected]
theorem int.div_nonpos {a b : ℤ} (Ha : 0 ≤ a) (Hb : b ≤ 0) :
a / b ≤ 0
source
theorem int.div_eq_zero_of_lt_abs {a b : ℤ} (H1 : 0 ≤ a) (H2 : a < |b|) :
a / b = 0
source
@[protected]
theorem int.add_mul_div_right (a b : ℤ) {c : ℤ} (H : c ≠ 0) :
(a + b * c) / c = a / c + b
source
@[protected]
theorem int.add_mul_div_left (a : ℤ) {b : ℤ} (c : ℤ) (H : b ≠ 0) :
(a + b * c) / b = a / b + c
source
@[protected, simp]
theorem int.mul_div_cancel (a : ℤ) {b : ℤ} (H : b ≠ 0) :
a * b / b = a
source
@[protected, simp]
theorem int.mul_div_cancel_left {a : ℤ} (b : ℤ) (H : a ≠ 0) :
a * b / a = b
source
@[protected, simp]
theorem int.div_self {a : ℤ} (H : a ≠ 0) :
a / a = 1
source
@[protected]
theorem int.add_div_of_dvd_right {a b c : ℤ} (H : c ∣ b) :
(a + b) / c = a / c + b / c
source
@[protected]
theorem int.add_div_of_dvd_left {a b c : ℤ} (H : c ∣ a) :
(a + b) / c = a / c + b / c

mod #

source
@[simp]
theorem int.mod_abs (a b : ℤ) :
a % |b| = a % b
source
theorem int.mod_nonneg (a : ℤ) {b : ℤ} :
b ≠ 0 → 0 ≤ a % b
source
theorem int.mod_lt_of_pos (a : ℤ) {b : ℤ} (H : 0 < b) :
a % b < b
source
theorem int.mod_lt (a : ℤ) {b : ℤ} (H : b ≠ 0) :
a % b < |b|
source
@[simp]
theorem int.add_mul_mod_self {a b c : ℤ} :
(a + b * c) % c = a % c
source
@[simp]
theorem int.add_mul_mod_self_left (a b c : ℤ) :
(a + b * c) % b = a % b
source
@[simp]
theorem int.add_mod_self {a b : ℤ} :
(a + b) % b = a % b
source
@[simp]
theorem int.add_mod_self_left {a b : ℤ} :
(a + b) % a = b % a
source
@[simp]
theorem int.mod_add_mod (m n k : ℤ) :
(m % n + k) % n = (m + k) % n
source
@[simp]
theorem int.add_mod_mod (m n k : ℤ) :
(m + n % k) % k = (m + n) % k
source
theorem int.add_mod (a b n : ℤ) :
(a + b) % n = (a % n + b % n) % n
source
theorem int.add_mod_eq_add_mod_right {m n k : ℤ} (i : ℤ) (H : m % n = k % n) :
(m + i) % n = (k + i) % n
source
theorem int.add_mod_eq_add_mod_left {m n k : ℤ} (i : ℤ) (H : m % n = k % n) :
(i + m) % n = (i + k) % n
source
theorem int.mod_add_cancel_right {m n k : ℤ} (i : ℤ) :
(m + i) % n = (k + i) % n ↔ m % n = k % n
source
theorem int.mod_add_cancel_left {m n k i : ℤ} :
(i + m) % n = (i + k) % n ↔ m % n = k % n
source
theorem int.mod_sub_cancel_right {m n k : ℤ} (i : ℤ) :
(m - i) % n = (k - i) % n ↔ m % n = k % n
source
@[simp]
theorem int.mul_mod_left (a b : ℤ) :
a * b % b = 0
source
@[simp]
theorem int.mul_mod_right (a b : ℤ) :
a * b % a = 0
source
theorem int.mul_mod (a b n : ℤ) :
a * b % n = a % n * (b % n) % n
source
theorem int.mod_self {a : ℤ} :
a % a = 0
source
@[simp]
theorem int.mod_mod_of_dvd (n : ℤ) {m k : ℤ} (h : m ∣ k) :
n % k % m = n % m
source
@[simp]
theorem int.mod_mod (a b : ℤ) :
a % b % b = a % b
source
theorem int.sub_mod (a b n : ℤ) :
(a - b) % n = (a % n - b % n) % n
source
@[protected]
theorem int.div_mod_unique {a b r q : ℤ} (h : 0 < b) :
a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < b

See also int.div_mod_equiv for a similar statement as an equiv.

source
theorem int.mod_eq_mod_iff_mod_sub_eq_zero {m n k : ℤ} :
m % n = k % n ↔ (m - k) % n = 0
source
@[simp]
theorem int.neg_mod_two (i : ℤ) :
-i % 2 = i % 2

properties of / and % #

source
theorem int.lt_div_add_one_mul_self (a : ℤ) {b : ℤ} (H : 0 < b) :
a < (a / b + 1) * b
source
theorem int.abs_div_le_abs (a b : ℤ) :
|a / b| ≤ |a|
source
theorem int.div_le_self {a : ℤ} (b : ℤ) (Ha : 0 ≤ a) :
a / b ≤ a
source
theorem int.mod_two_eq_zero_or_one (n : ℤ) :
n % 2 = 0 ∨ n % 2 = 1

dvd #

source
theorem int.dvd_of_mod_eq_zero {a b : ℤ} (H : b % a = 0) :
a ∣ b
source
theorem int.mod_eq_zero_of_dvd {a b : ℤ} :
a ∣ b → b % a = 0
source
theorem int.dvd_iff_mod_eq_zero (a b : ℤ) :
a ∣ b ↔ b % a = 0
source
theorem int.dvd_sub_of_mod_eq {a b c : ℤ} (h : a % b = c) :
b ∣ a - c

If a % b = c then b divides a - c.

source
theorem int.nat_abs_dvd {a b : ℤ} :
↑(a.nat_abs) ∣ b ↔ a ∣ b
source
theorem int.dvd_nat_abs {a b : ℤ} :
a ∣ ↑(b.nat_abs) ↔ a ∣ b
source
@[protected, instance]
def int.decidable_dvd  :
decidable_rel has_dvd.dvd
Equations
source
@[protected]
theorem int.div_mul_cancel {a b : ℤ} (H : b ∣ a) :
a / b * b = a
source
@[protected]
theorem int.mul_div_cancel' {a b : ℤ} (H : a ∣ b) :
a * (b / a) = b
source
theorem int.div_dvd_div {a b c : ℤ} (H1 : a ∣ b) (H2 : b ∣ c) :
b / a ∣ c / a
source
@[protected]
theorem int.eq_mul_of_div_eq_right {a b c : ℤ} (H1 : b ∣ a) (H2 : a / b = c) :
a = b * c
source
@[protected]
theorem int.div_eq_of_eq_mul_right {a b c : ℤ} (H1 : b ≠ 0) (H2 : a = b * c) :
a / b = c
source
@[protected]
theorem int.eq_div_of_mul_eq_right {a b c : ℤ} (H1 : a ≠ 0) (H2 : a * b = c) :
b = c / a
source
@[protected]
theorem int.div_eq_iff_eq_mul_right {a b c : ℤ} (H : b ≠ 0) (H' : b ∣ a) :
a / b = c ↔ a = b * c
source
@[protected]
theorem int.div_eq_iff_eq_mul_left {a b c : ℤ} (H : b ≠ 0) (H' : b ∣ a) :
a / b = c ↔ a = c * b
source
@[protected]
theorem int.eq_mul_of_div_eq_left {a b c : ℤ} (H1 : b ∣ a) (H2 : a / b = c) :
a = c * b
source
@[protected]
theorem int.div_eq_of_eq_mul_left {a b c : ℤ} (H1 : b ≠ 0) (H2 : a = c * b) :
a / b = c
source
@[protected]
theorem int.eq_zero_of_div_eq_zero {d n : ℤ} (h : d ∣ n) (H : n / d = 0) :
n = 0
source
@[protected, simp]
theorem int.div_left_inj {a b d : ℤ} (hda : d ∣ a) (hdb : d ∣ b) :
a / d = b / d ↔ a = b
source
theorem int.abs_sign_of_nonzero {z : ℤ} (hz : z ≠ 0) :
|z.sign| = 1
source
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.

source
@[protected]
theorem int.mul_div_assoc (a : ℤ) {b c : ℤ} :
c ∣ b → a * b / c = a * (b / c)
source
@[protected]
theorem int.mul_div_assoc' (b : ℤ) {a c : ℤ} (h : c ∣ a) :
a * b / c = a / c * b
source
theorem int.neg_div_of_dvd {a b : ℤ} (H : b ∣ a) :
-a / b = -(a / b)
source
theorem int.sub_div_of_dvd (a : ℤ) {b c : ℤ} (hcb : c ∣ b) :
(a - b) / c = a / c - b / c
source
theorem int.sub_div_of_dvd_sub {a b c : ℤ} (hcab : c ∣ a - b) :
(a - b) / c = a / c - b / c
source
@[protected]
theorem int.sign_eq_div_abs (a : ℤ) :
a.sign = a / |a|

/ and ordering #

source
@[protected]
theorem int.div_mul_le (a : ℤ) {b : ℤ} (H : b ≠ 0) :
a / b * b ≤ a
source
@[protected]
theorem int.div_le_of_le_mul {a b c : ℤ} (H : 0 < c) (H' : a ≤ b * c) :
a / c ≤ b
source
@[protected]
theorem int.mul_lt_of_lt_div {a b c : ℤ} (H : 0 < c) (H3 : a < b / c) :
a * c < b
source
@[protected]
theorem int.mul_le_of_le_div {a b c : ℤ} (H1 : 0 < c) (H2 : a ≤ b / c) :
a * c ≤ b
source
@[protected]
theorem int.le_div_of_mul_le {a b c : ℤ} (H1 : 0 < c) (H2 : a * c ≤ b) :
a ≤ b / c
source
@[protected]
theorem int.le_div_iff_mul_le {a b c : ℤ} (H : 0 < c) :
a ≤ b / c ↔ a * c ≤ b
source
@[protected]
theorem int.div_le_div {a b c : ℤ} (H : 0 < c) (H' : a ≤ b) :
a / c ≤ b / c
source
@[protected]
theorem int.div_lt_of_lt_mul {a b c : ℤ} (H : 0 < c) (H' : a < b * c) :
a / c < b
source
@[protected]
theorem int.lt_mul_of_div_lt {a b c : ℤ} (H1 : 0 < c) (H2 : a / c < b) :
a < b * c
source
@[protected]
theorem int.div_lt_iff_lt_mul {a b c : ℤ} (H : 0 < c) :
a / c < b ↔ a < b * c
source
@[protected]
theorem int.le_mul_of_div_le {a b c : ℤ} (H1 : 0 ≤ b) (H2 : b ∣ a) (H3 : a / b ≤ c) :
a ≤ c * b
source
@[protected]
theorem int.lt_div_of_mul_lt {a b c : ℤ} (H1 : 0 ≤ b) (H2 : b ∣ c) (H3 : a * b < c) :
a < c / b
source
@[protected]
theorem int.lt_div_iff_mul_lt {a b : ℤ} (c : ℤ) (H : 0 < c) (H' : c ∣ b) :
a < b / c ↔ a * c < b
source
theorem int.div_pos_of_pos_of_dvd {a b : ℤ} (H1 : 0 < a) (H2 : 0 ≤ b) (H3 : b ∣ a) :
0 < a / b
source
theorem int.nat_abs_eq_of_dvd_dvd {s t : ℤ} (hst : s ∣ t) (hts : t ∣ s) :
s.nat_abs = t.nat_abs
source
theorem int.div_eq_div_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
source
theorem int.div_dvd_of_dvd {s t : ℤ} (hst : s ∣ t) :
t / s ∣ t

to_nat #

source
@[simp]
theorem int.to_nat_le {a : ℤ} {n : ℕ} :
a.to_nat ≤ n ↔ a ≤ ↑n
source
@[simp]
theorem int.lt_to_nat {n : ℕ} {a : ℤ} :
n < a.to_nat ↔ ↑n < a
source
@[simp]
theorem int.coe_nat_nonpos_iff {n : ℕ} :
↑n ≤ 0 ↔ n = 0
source
theorem int.to_nat_le_to_nat {a b : ℤ} (h : a ≤ b) :
a.to_nat ≤ b.to_nat
source
theorem int.to_nat_lt_to_nat {a b : ℤ} (hb : 0 < b) :
a.to_nat < b.to_nat ↔ a < b
source
theorem int.lt_of_to_nat_lt {a b : ℤ} (h : a.to_nat < b.to_nat) :
a < b
source
@[simp]
theorem int.to_nat_pred_coe_of_pos {i : ℤ} (h : 0 < i) :
↑(i.to_nat - 1) = i - 1
source
@[simp]
theorem int.to_nat_eq_zero {n : ℤ} :
n.to_nat = 0 ↔ n ≤ 0
source
@[simp]
theorem int.to_nat_sub_of_le {a b : ℤ} (h : b ≤ a) :
↑((a - b).to_nat) = a - b