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 #

@[protected, instance]
Equations

Extra instances to short-circuit type class resolution #

theorem int.abs_eq_nat_abs (a : ) :
@[simp, norm_cast]
theorem int.coe_nat_abs (n : ) :
theorem nat.cast_nat_abs {α : Type u_1} [add_group_with_one α] (n : ) :
theorem int.nat_abs_abs (a : ) :
theorem int.sign_mul_abs (a : ) :
a.sign * |a| = a
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
@[norm_cast]
theorem int.abs_coe_nat (n : ) :
theorem int.sign_add_eq_of_sign_eq {m n : } :
m.sign = n.sign (m + n).sign = n.sign

succ and pred #

theorem int.lt_succ_self (a : ) :
a < a.succ
theorem int.pred_self_lt (a : ) :
a.pred < a
theorem int.lt_add_one_iff {a b : } :
a < b + 1 a b
theorem int.le_add_one {a b : } (h : a b) :
a b + 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|
@[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
@[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.

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

@[simp]
theorem int.nat_abs_dvd_iff_dvd {a b : } :

/ #

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

mod #

@[simp]
theorem int.mod_abs (a b : ) :
a % |b| = a % b
theorem int.mod_nonneg (a : ) {b : } :
b 0 0 a % b
theorem int.mod_lt_of_pos (a : ) {b : } (H : 0 < b) :
a % b < b
theorem int.mod_lt (a : ) {b : } (H : b 0) :
a % b < |b|
@[simp]
theorem int.add_mul_mod_self {a b c : } :
(a + b * c) % c = a % c
@[simp]
theorem int.add_mul_mod_self_left (a b c : ) :
(a + b * c) % b = a % b
@[simp]
theorem int.add_mod_self {a b : } :
(a + b) % b = a % b
@[simp]
theorem int.add_mod_self_left {a b : } :
(a + b) % a = b % a
@[simp]
theorem int.mod_add_mod (m n k : ) :
(m % n + k) % n = (m + k) % n
@[simp]
theorem int.add_mod_mod (m n k : ) :
(m + n % k) % k = (m + n) % k
theorem int.add_mod (a b n : ) :
(a + b) % n = (a % n + b % n) % n
theorem int.add_mod_eq_add_mod_right {m n k : } (i : ) (H : m % n = k % n) :
(m + i) % n = (k + i) % n
theorem int.add_mod_eq_add_mod_left {m n k : } (i : ) (H : m % n = k % n) :
(i + m) % n = (i + k) % n
theorem int.mod_add_cancel_right {m n k : } (i : ) :
(m + i) % n = (k + i) % n m % n = k % n
theorem int.mod_add_cancel_left {m n k i : } :
(i + m) % n = (i + k) % n m % n = k % n
theorem int.mod_sub_cancel_right {m n k : } (i : ) :
(m - i) % n = (k - i) % n m % n = k % n
@[simp]
theorem int.mul_mod_left (a b : ) :
a * b % b = 0
@[simp]
theorem int.mul_mod_right (a b : ) :
a * b % a = 0
theorem int.mul_mod (a b n : ) :
a * b % n = a % n * (b % n) % n
theorem int.mod_self {a : } :
a % a = 0
@[simp]
theorem int.mod_mod_of_dvd (n : ) {m k : } (h : m k) :
n % k % m = n % m
@[simp]
theorem int.mod_mod (a b : ) :
a % b % b = a % b
theorem int.sub_mod (a b n : ) :
(a - b) % n = (a % n - b % n) % n
@[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.

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

properties of / and % #

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

dvd #

theorem int.dvd_of_mod_eq_zero {a b : } (H : b % a = 0) :
a b
theorem int.mod_eq_zero_of_dvd {a b : } :
a b b % a = 0
theorem int.dvd_iff_mod_eq_zero (a b : ) :
a b b % a = 0
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.

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

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

/ and ordering #

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

to_nat #

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