data.int.basic

Basic operations on the integers #

This file contains:

• instances on ℤ. The stronger one is int.linear_ordered_comm_ring.
• some basic lemmas about integers

Recursors #

• int.rec: Sign disjunction. Something is true/defined on ℤ if it's true/defined for nonnegative and for negative values.
• int.bit_cases_on: Parity disjunction. Something is true/defined on ℤ if it's true/defined for even and for odd values.
• int.induction_on: Simple growing induction on positive numbers, plus simple decreasing induction on negative numbers. Note that this recursor is currently only Prop-valued.
• int.induction_on': Simple growing induction for numbers greater than b, plus simple decreasing induction on numbers less than b.
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations

Extra instances to short-circuit type class resolution #

These also prevent non-computable instances like int.normed_comm_ring being used to construct these instances non-computably.

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def int.monoid  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def int.ring  :
Equations
@[protected, instance]
def int.distrib  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem int.add_neg_one (i : ) :
i + -1 = i - 1
theorem int.abs_eq_nat_abs (a : ) :
theorem int.nat_abs_abs (a : ) :
theorem int.sign_mul_abs (a : ) :
(a.sign) * |a| = a
@[simp]
theorem int.default_eq_zero  :
@[protected, instance]
meta def int.has_to_format  :
@[protected, instance]
meta def int.has_reflect  :
@[simp]
theorem int.add_def {a b : } :
a.add b = a + b
@[simp]
theorem int.mul_def {a b : } :
a.mul b = a * b
@[simp]
theorem int.neg_succ_not_nonneg (n : ) :
@[simp]
theorem int.neg_succ_not_pos (n : ) :
@[simp]
theorem int.neg_succ_sub_one (n : ) :
- 1 = -[1+ n + 1]
@[simp]
theorem int.coe_nat_mul_neg_succ (m n : ) :
(m) * = -(m) * (n.succ)
@[simp]
theorem int.neg_succ_mul_coe_nat (m n : ) :
* n = -((m.succ)) * n
@[simp]
theorem int.neg_succ_mul_neg_succ (m n : ) :
* = ((m.succ)) * (n.succ)
@[simp, norm_cast]
theorem int.coe_nat_le {m n : } :
m n m n
@[simp, norm_cast]
theorem int.coe_nat_lt {m n : } :
m < n m < n
@[simp, norm_cast]
theorem int.coe_nat_inj' {m n : } :
m = n m = n
@[simp]
theorem int.coe_nat_pos {n : } :
0 < n 0 < n
@[simp]
theorem int.coe_nat_eq_zero {n : } :
n = 0 n = 0
theorem int.coe_nat_ne_zero {n : } :
n 0 n 0
@[simp]
theorem int.coe_nat_nonneg (n : ) :
0 n
theorem int.le_coe_nat_sub (m n : ) :
m - n (m - n)
theorem int.coe_nat_ne_zero_iff_pos {n : } :
n 0 0 < n
theorem int.coe_nat_succ_pos (n : ) :
0 < (n.succ)
@[simp, norm_cast]
theorem int.coe_nat_abs (n : ) :

succ and pred #

def int.succ (a : ) :

Immediate successor of an integer: succ n = n + 1

Equations
def int.pred (a : ) :

Immediate predecessor of an integer: pred n = n - 1

Equations
theorem int.pred_succ (a : ) :
a.succ.pred = a
theorem int.succ_pred (a : ) :
a.pred.succ = a
theorem int.neg_succ (a : ) :
-a.succ = (-a).pred
theorem int.succ_neg_succ (a : ) :
(-a.succ).succ = -a
theorem int.neg_pred (a : ) :
-a.pred = (-a).succ
theorem int.pred_neg_pred (a : ) :
(-a.pred).pred = -a
theorem int.pred_nat_succ (n : ) :
theorem int.neg_nat_succ (n : ) :
theorem int.succ_neg_nat_succ (n : ) :
theorem int.lt_succ_self (a : ) :
a < a.succ
theorem int.pred_self_lt (a : ) :
a.pred < a
theorem int.add_one_le_iff {a b : } :
a + 1 b a < b
theorem int.lt_add_one_iff {a b : } :
a < b + 1 a b
@[simp]
theorem int.succ_coe_nat_pos (n : ) :
0 < n + 1
@[norm_cast]
theorem int.coe_pred_of_pos {n : } (h : 0 < n) :
(n - 1) = n - 1
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.eq_zero_iff_abs_lt_one {a : } :
|a| < 1 a = 0
@[protected]
theorem int.induction_on {p : → Prop} (i : ) (hz : p 0) (hp : ∀ (i : ), p ip (i + 1)) (hn : ∀ (i : ), p (-i)p (-i - 1)) :
p i
@[protected]
def int.induction_on' {C : Sort u_1} (z b : ) :
C b(Π (k : ), b kC kC (k + 1))(Π (k : ), k bC kC (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

nat abs #

theorem int.nat_abs_add_le (a b : ) :
theorem int.nat_abs_sub_le (a b : ) :
theorem int.nat_abs_neg_of_nat (n : ) :
= n
theorem int.nat_abs_mul (a b : ) :
(a * b).nat_abs = (a.nat_abs) * b.nat_abs
theorem int.nat_abs_mul_nat_abs_eq {a b : } {c : } (h : a * b = c) :
(a.nat_abs) * b.nat_abs = c
@[simp]
theorem int.nat_abs_mul_self' (a : ) :
((a.nat_abs)) * (a.nat_abs) = a * a
theorem int.neg_succ_of_nat_eq' (m : ) :
= -m - 1
theorem int.nat_abs_ne_zero_of_ne_zero {z : } (hz : z 0) :
@[simp]
theorem int.nat_abs_eq_zero {a : } :
a.nat_abs = 0 a = 0
theorem int.nat_abs_ne_zero {a : } :
a.nat_abs 0 a 0
theorem int.nat_abs_lt_nat_abs_of_nonneg_of_lt {a b : } (w₁ : 0 a) (w₂ : a < b) :
theorem int.nat_abs_eq_nat_abs_iff {a b : } :
a.nat_abs = b.nat_abs a = b a = -b
theorem int.nat_abs_eq_iff {a : } {n : } :
a.nat_abs = n a = n a = -n
theorem int.nat_abs_eq_iff_mul_self_eq {a b : } :
a.nat_abs = b.nat_abs a * a = b * b
theorem int.nat_abs_lt_iff_mul_self_lt {a b : } :
a.nat_abs < b.nat_abs a * a < b * b
theorem int.nat_abs_eq_iff_sq_eq {a b : } :
a.nat_abs = b.nat_abs a ^ 2 = b ^ 2
theorem int.nat_abs_lt_iff_sq_lt {a b : } :
a.nat_abs < b.nat_abs a ^ 2 < b ^ 2
theorem int.nat_abs_le_iff_sq_le {a b : } :
a.nat_abs b.nat_abs a ^ 2 b ^ 2
@[simp]
theorem int.nat_abs_dvd_iff_dvd {a b : } :
theorem int.nat_abs_inj_of_nonneg_of_nonneg {a b : } (ha : 0 a) (hb : 0 b) :
theorem int.nat_abs_inj_of_nonpos_of_nonpos {a b : } (ha : a 0) (hb : b 0) :
theorem int.nat_abs_inj_of_nonneg_of_nonpos {a b : } (ha : 0 a) (hb : b 0) :
theorem int.nat_abs_inj_of_nonpos_of_nonneg {a b : } (ha : a 0) (hb : 0 b) :

/#

@[simp]
theorem int.of_nat_div (m n : ) :
int.of_nat (m / n) =
@[simp, norm_cast]
theorem int.coe_nat_div (m n : ) :
(m / n) = m / n
theorem int.neg_succ_of_nat_div (m : ) {b : } (H : 0 < b) :
/ b = -(m / b + 1)
@[protected]
theorem int.zero_div (b : ) :
0 / b = 0
@[protected]
theorem int.div_zero (a : ) :
a / 0 = 0
@[protected, simp]
theorem int.div_neg (a b : ) :
a / -b = -(a / b)
theorem int.div_of_neg_of_pos {a b : } (Ha : a < 0) (Hb : 0 < b) :
a / b = -((-a - 1) / b + 1)
@[protected]
theorem int.div_nonneg {a b : } (Ha : 0 a) (Hb : 0 b) :
0 a / b
@[protected]
theorem int.div_nonpos {a b : } (Ha : 0 a) (Hb : b 0) :
a / b 0
theorem int.div_neg' {a b : } (Ha : a < 0) (Hb : 0 < b) :
a / b < 0
@[protected, simp]
theorem int.div_one (a : ) :
a / 1 = a
theorem int.div_eq_zero_of_lt {a b : } (H1 : 0 a) (H2 : a < b) :
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]
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
@[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

mod #

theorem int.of_nat_mod (m n : ) :
m % n = int.of_nat (m % n)
@[simp, norm_cast]
theorem int.coe_nat_mod (m n : ) :
(m % n) = m % n
theorem int.neg_succ_of_nat_mod (m : ) {b : } (bpos : 0 < b) :
% b = b - 1 - m % b
@[simp]
theorem int.mod_neg (a b : ) :
a % -b = a % b
@[simp]
theorem int.mod_abs (a b : ) :
a % |b| = a % b
theorem int.zero_mod (b : ) :
0 % b = 0
theorem int.mod_zero (a : ) :
a % 0 = a
theorem int.mod_one (a : ) :
a % 1 = 0
theorem int.mod_eq_of_lt {a b : } (H1 : 0 a) (H2 : a < b) :
a % b = a
theorem int.mod_nonneg (a : ) {b : } :
b 00 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|
theorem int.mod_add_div_aux (m n : ) :
n - (m % n + 1) - ((n) * (m / n) + n) =
theorem int.mod_add_div (a b : ) :
a % b + b * (a / b) = a
theorem int.div_add_mod (a b : ) :
b * (a / b) + a % b = a
theorem int.mod_add_div' (m k : ) :
m % k + (m / k) * k = m
theorem int.div_add_mod' (m k : ) :
(m / k) * k + m % k = m
theorem int.mod_def (a b : ) :
a % b = a - b * (a / 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
theorem int.mod_eq_mod_iff_mod_sub_eq_zero {m n k : } :
m % n = k % n (m - k) % n = 0
@[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
@[simp]
theorem int.neg_mod_two (i : ) :
-i % 2 = i % 2
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

properties of / and %#

@[simp]
theorem int.mul_div_mul_of_pos {a : } (b c : ) (H : 0 < a) :
a * b / a * c = b / c
@[simp]
theorem int.mul_div_mul_of_pos_left (a : ) {b : } (H : 0 < b) (c : ) :
a * b / c * b = a / c
@[simp]
theorem int.mul_mod_mul_of_pos {a : } (H : 0 < a) (b c : ) :
a * b % a * c = a * (b % c)
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.mul_div_cancel_of_mod_eq_zero {a b : } (H : a % b = 0) :
b * (a / b) = a
theorem int.div_mul_cancel_of_mod_eq_zero {a b : } (H : a % b = 0) :
(a / b) * b = a
theorem int.mod_two_eq_zero_or_one (n : ) :
n % 2 = 0 n % 2 = 1

dvd #

@[norm_cast]
theorem int.coe_nat_dvd {m n : } :
m n m n
theorem int.coe_nat_dvd_left {n : } {z : } :
theorem int.coe_nat_dvd_right {n : } {z : } :
theorem int.dvd_antisymm {a b : } (H1 : 0 a) (H2 : 0 b) :
a bb aa = b
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 bb % 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
@[protected]
theorem int.mul_div_assoc (a : ) {b c : } :
c ba * 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.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
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
theorem int.nat_abs_sign (z : ) :
z.sign.nat_abs = ite (z = 0) 0 1
theorem int.nat_abs_sign_of_nonzero {z : } (hz : z 0) :
theorem int.abs_sign_of_nonzero {z : } (hz : z 0) :
|z.sign| = 1
theorem int.sign_coe_nat_of_nonzero {n : } (hn : n 0) :
@[simp]
theorem int.sign_neg (z : ) :
(-z).sign = -z.sign
theorem int.div_sign (a b : ) :
a / b.sign = a * b.sign
@[simp]
theorem int.sign_mul (a b : ) :
(a * b).sign = (a.sign) * b.sign
@[protected]
theorem int.sign_eq_div_abs (a : ) :
a.sign = a / |a|
theorem int.mul_sign (i : ) :
i * i.sign = (i.nat_abs)
@[simp]
theorem int.sign_pow_bit1 (k : ) (n : ) :
n.sign ^ bit1 k = n.sign
theorem int.le_of_dvd {a b : } (bpos : 0 < b) (H : a b) :
a b
theorem int.eq_one_of_dvd_one {a : } (H : 0 a) (H' : a 1) :
a = 1
theorem int.eq_one_of_mul_eq_one_right {a b : } (H : 0 a) (H' : a * b = 1) :
a = 1
theorem int.eq_one_of_mul_eq_one_left {a b : } (H : 0 b) (H' : a * b = 1) :
b = 1
theorem int.of_nat_dvd_of_dvd_nat_abs {a : } {z : } (haz : a z.nat_abs) :
a z
theorem int.dvd_nat_abs_of_of_nat_dvd {a : } {z : } (haz : a z) :
theorem int.pow_dvd_of_le_of_pow_dvd {p m n : } {k : } (hmn : m n) (hdiv : (p ^ n) k) :
(p ^ m) k
theorem int.dvd_of_pow_dvd {p k : } {m : } (hk : 1 k) (hpk : (p ^ k) m) :
p m
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.

/ 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.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.eq_mul_div_of_mul_eq_mul_of_dvd_left {a b c d : } (hb : b 0) (hbc : b c) (h : b * a = c * d) :
a = (c / b) * d
theorem int.eq_zero_of_dvd_of_nat_abs_lt_nat_abs {a b : } (w : a b) (h : b.nat_abs < a.nat_abs) :
b = 0

If an integer with larger absolute value divides an integer, it is zero.

theorem int.eq_zero_of_dvd_of_nonneg_of_lt {a b : } (w₁ : 0 a) (w₂ : a < b) (h : b a) :
a = 0
theorem int.eq_of_mod_eq_of_nat_abs_sub_lt_nat_abs {a b c : } (h1 : a % b = c) (h2 : (a - c).nat_abs < b.nat_abs) :
a = c

If two integers are congruent to a sufficiently large modulus, they are equal.

theorem int.of_nat_add_neg_succ_of_nat_of_lt {m n : } (h : m < n.succ) :
+ = -[1+ n - m]
theorem int.of_nat_add_neg_succ_of_nat_of_ge {m n : } (h : n.succ m) :
@[simp]
theorem int.neg_add_neg (m n : ) :
+ = -[1+ (m + n).succ]
theorem int.nat_abs_le_of_dvd_ne_zero {s t : } (hst : s t) (ht : t 0) :
theorem int.nat_abs_eq_of_dvd_dvd {s t : } (hst : s t) (hts : t s) :
theorem int.div_dvd_of_ne_zero_dvd {s t : } (hst : s t) :
t / s t

to_nat #

theorem int.to_nat_eq_max (a : ) :
(a.to_nat) = max a 0
@[simp]
theorem int.to_nat_zero  :
0.to_nat = 0
@[simp]
theorem int.to_nat_one  :
1.to_nat = 1
@[simp]
theorem int.to_nat_of_nonneg {a : } (h : 0 a) :
(a.to_nat) = a
@[simp]
theorem int.to_nat_sub_of_le {a b : } (h : b a) :
((a - b).to_nat) = a - b
@[simp]
theorem int.to_nat_coe_nat (n : ) :
@[simp]
theorem int.to_nat_coe_nat_add_one {n : } :
(n + 1).to_nat = n + 1
theorem int.le_to_nat (a : ) :
@[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.le_to_nat_iff {n : } {z : } (h : 0 z) :
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
theorem int.to_nat_add {a b : } (ha : 0 a) (hb : 0 b) :
(a + b).to_nat = a.to_nat + b.to_nat
theorem int.to_nat_add_nat {a : } (ha : 0 a) (n : ) :
(a + n).to_nat = a.to_nat + n
@[simp]
theorem int.pred_to_nat (i : ) :
(i - 1).to_nat = i.to_nat - 1
@[simp]
theorem int.to_nat_pred_coe_of_pos {i : } (h : 0 < i) :
(i.to_nat - 1) = i - 1
@[simp]
theorem int.to_nat_sub_to_nat_neg (n : ) :
(n.to_nat) - ((-n).to_nat) = n
def int.to_nat'  :

If n : ℕ, then int.to_nat' n = some n, if n : ℤ is negative, then int.to_nat' n = none.

Equations
theorem int.mem_to_nat' (a : ) (n : ) :
theorem int.to_nat_of_nonpos {z : } :
z 0z.to_nat = 0

units #

@[simp]
theorem int.units_nat_abs (u : ˣ) :
theorem int.units_eq_one_or (u : ˣ) :
u = 1 u = -1
theorem int.is_unit_eq_one_or {a : } :
a = 1 a = -1
theorem int.is_unit_iff {a : } :
a = 1 a = -1
theorem int.is_unit_iff_abs_eq {x : } :
|x| = 1
@[norm_cast]
theorem int.of_nat_is_unit {n : } :
theorem int.units_inv_eq_self (u : ˣ) :
u⁻¹ = u
@[simp]
theorem int.units_mul_self (u : ˣ) :
u * u = 1
@[simp]
theorem int.units_coe_mul_self (u : ˣ) :
(u) * u = 1
@[simp]
theorem int.neg_one_pow_ne_zero {n : } :
(-1) ^ n 0

bitwise ops #

@[simp]
theorem int.bodd_zero  :
@[simp]
theorem int.bodd_one  :
theorem int.bodd_two  :
@[simp, norm_cast]
theorem int.bodd_coe (n : ) :
@[simp]
theorem int.bodd_sub_nat_nat (m n : ) :
n).bodd = bxor m.bodd n.bodd
@[simp]
theorem int.bodd_neg_of_nat (n : ) :
@[simp]
theorem int.bodd_neg (n : ) :
(-n).bodd = n.bodd
@[simp]
theorem int.bodd_add (m n : ) :
(m + n).bodd = bxor m.bodd n.bodd
@[simp]
theorem int.bodd_mul (m n : ) :
(m * n).bodd = m.bodd && n.bodd
theorem int.bodd_add_div2 (n : ) :
cond n.bodd 1 0 + 2 * n.div2 = n
theorem int.div2_val (n : ) :
n.div2 = n / 2
theorem int.bit0_val (n : ) :
bit0 n = 2 * n
theorem int.bit1_val (n : ) :
bit1 n = 2 * n + 1
theorem int.bit_val (b : bool) (n : ) :
n = 2 * n + cond b 1 0
theorem int.bit_decomp (n : ) :
n.div2 = n
def int.bit_cases_on {C : Sort u} (n : ) (h : Π (b : bool) (n : ), C (int.bit b n)) :
C n

Defines a function from ℤ conditionally, if it is defined for odd and even integers separately using bit.

Equations
@[simp]
theorem int.bit_zero  :
= 0
@[simp]
theorem int.bit_coe_nat (b : bool) (n : ) :
n = (nat.bit b n)
@[simp]
theorem int.bit_neg_succ (b : bool) (n : ) :
@[simp]
theorem int.bodd_bit (b : bool) (n : ) :
(int.bit b n).bodd = b
@[simp]
theorem int.bodd_bit0 (n : ) :
@[simp]
theorem int.bodd_bit1 (n : ) :
@[simp]
theorem int.div2_bit (b : bool) (n : ) :
(int.bit b n).div2 = n
theorem int.bit0_ne_bit1 (m n : ) :
theorem int.bit1_ne_bit0 (m n : ) :
theorem int.bit1_ne_zero (m : ) :
bit1 m 0
@[simp]
theorem int.test_bit_zero (b : bool) (n : ) :
(int.bit b n).test_bit 0 = b
@[simp]
theorem int.test_bit_succ (m : ) (b : bool) (n : ) :
theorem int.bitwise_or  :
theorem int.bitwise_and  :
theorem int.bitwise_diff  :
int.bitwise (λ (a b : bool), a && !b) = int.ldiff
theorem int.bitwise_xor  :
@[simp]
theorem int.bitwise_bit (f : bool) (a : bool) (m : ) (b : bool) (n : ) :
(int.bit a m) (int.bit b n) = int.bit (f a b) m n)
@[simp]
theorem int.lor_bit (a : bool) (m : ) (b : bool) (n : ) :
(int.bit a m).lor (int.bit b n) = int.bit (a || b) (m.lor n)
@[simp]
theorem int.land_bit (a : bool) (m : ) (b : bool) (n : ) :
(int.bit a m).land (int.bit b n) = int.bit (a && b) (m.land n)
@[simp]
theorem int.ldiff_bit (a : bool) (m : ) (b : bool) (n : ) :
(int.bit a m).ldiff (int.bit b n) = int.bit (a && !b) (m.ldiff n)
@[simp]
theorem int.lxor_bit (a : bool) (m : ) (b : bool) (n : ) :
(int.bit a m).lxor (int.bit b n) = int.bit (bxor a b) (m.lxor n)
@[simp]
theorem int.lnot_bit (b : bool) (n : ) :
(int.bit b n).lnot = int.bit (!b) n.lnot
@[simp]
theorem int.test_bit_bitwise (f : bool) (m n : ) (k : ) :
m n).test_bit k = f (m.test_bit k) (n.test_bit k)
@[simp]
theorem int.test_bit_lor (m n : ) (k : ) :
(m.lor n).test_bit k = m.test_bit k || n.test_bit k
@[simp]
theorem int.test_bit_land (m n : ) (k : ) :
(m.land n).test_bit k = m.test_bit k && n.test_bit k
@[simp]
theorem int.test_bit_ldiff (m n : ) (k : ) :
@[simp]
theorem int.test_bit_lxor (m n : ) (k : ) :
(m.lxor n).test_bit k = bxor (m.test_bit k) (n.test_bit k)
@[simp]
theorem int.test_bit_lnot (n : ) (k : ) :
theorem int.shiftl_add (m : ) (n : ) (k : ) :
m.shiftl (n + k) = (m.shiftl n).shiftl k
theorem int.shiftl_sub (m : ) (n : ) (k : ) :
m.shiftl (n - k) = (m.shiftl n).shiftr k
@[simp]
theorem int.shiftl_neg (m n : ) :
m.shiftl (-n) = m.shiftr n
@[simp]
theorem int.shiftr_neg (m n : ) :
m.shiftr (-n) = m.shiftl n
@[simp]
theorem int.shiftl_coe_nat (m n : ) :
@[simp]
theorem int.shiftr_coe_nat (m n : ) :
@[simp]
theorem int.shiftl_neg_succ (m n : ) :
@[simp]
theorem int.shiftr_neg_succ (m n : ) :
theorem int.shiftr_add (m : ) (n k : ) :
theorem int.shiftl_eq_mul_pow (m : ) (n : ) :
m.shiftl n = m * (2 ^ n)
theorem int.shiftr_eq_div_pow (m : ) (n : ) :
m.shiftr n = m / (2 ^ n)
theorem int.one_shiftl (n : ) :
1.shiftl n = (2 ^ n)
@[simp]
theorem int.zero_shiftl (n : ) :
0.shiftl n = 0
@[simp]
theorem int.zero_shiftr (n : ) :
0.shiftr n = 0