mathlib documentation

data.int.basic

Basic instances on the integers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. https://github.com/leanprover-community/mathlib4/pull/584 Any changes to this file require a corresponding PR to mathlib4.

This file contains:

@[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.ring  :
Equations
@[protected, instance]
Equations
@[simp]
theorem int.add_neg_one (i : ) :
i + -1 = i - 1
@[protected, instance]
@[protected, instance]
meta def int.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+ n] - 1 = -[1+ n + 1]
@[simp]
theorem int.coe_nat_mul_neg_succ (m n : ) :
m * -[1+ n] = -(m * (n.succ))
@[simp]
theorem int.neg_succ_mul_coe_nat (m n : ) :
-[1+ m] * n = -((m.succ) * n)
@[simp]
theorem int.neg_succ_mul_neg_succ (m n : ) :
-[1+ m] * -[1+ n] = (m.succ) * (n.succ)
theorem int.coe_nat_le {m n : } :
m n m n
theorem int.coe_nat_lt {m n : } :
m < n m < n
theorem int.coe_nat_inj' {m n : } :
m = n m = n
theorem int.coe_nat_nonneg (n : ) :
0 n
@[simp]
theorem int.neg_of_nat_ne_zero (n : ) :
@[simp]
theorem int.zero_ne_neg_of_nat (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.add_one_le_iff {a b : } :
a + 1 b a < b
@[norm_cast]
theorem int.coe_pred_of_pos {n : } (h : 0 < n) :
(n - 1) = n - 1
@[protected]
theorem int.induction_on {p : Prop} (i : ) (hz : p 0) (hp : (i : ), p i p (i + 1)) (hn : (i : ), p (-i) p (-i - 1)) :
p i

nat abs #

theorem int.nat_abs_add_le (a b : ) :
theorem int.nat_abs_sub_le (a b : ) :
theorem int.nat_abs_mul (a b : ) :
theorem int.nat_abs_mul_nat_abs_eq {a b : } {c : } (h : a * b = 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 : ) :
-[1+ 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

/ #

@[simp]
theorem int.of_nat_div (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) :
-[1+ m] / 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
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

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) :
-[1+ m] % b = b - 1 - m % b
@[simp]
theorem int.mod_neg (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_add_div_aux (m n : ) :
n - (m % n + 1) - (n * (m / n) + n) = -[1+ m]
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)

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.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.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.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
theorem int.mul_sign (i : ) :
i * i.sign = (i.nat_abs)
theorem int.of_nat_add_neg_succ_of_nat_of_lt {m n : } (h : m < n.succ) :
@[simp]
theorem int.neg_add_neg (m n : ) :
-[1+ m] + -[1+ n] = -[1+ (m + n).succ]

to_nat #

@[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_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.le_to_nat_iff {n : } {z : } (h : 0 z) :
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_sub_to_nat_neg (n : ) :
(n.to_nat) - ((-n).to_nat) = n

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 : ) :
@[simp]
theorem int.to_nat_neg_nat (n : ) :