mathlib documentation

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]

def int.inhabited :

Equations

int.inhabited = {default := int.zero}

@[protected, instance]

def int.nontrivial :

@[protected, instance]

def int.comm_ring :

Equations

int.comm_ring = {add := int.add, add_assoc := int.add_assoc, zero := int.zero, zero_add := int.zero_add, add_zero := int.add_zero, nsmul := ring.nsmul._default int.zero int.add int.zero_add int.add_zero, nsmul_zero' := int.comm_ring._proof_1, nsmul_succ' := int.comm_ring._proof_2, neg := int.neg, sub := int.sub, sub_eq_add_neg := int.comm_ring._proof_3, zsmul := has_mul.mul int.has_mul, zsmul_zero' := int.zero_mul, zsmul_succ' := int.comm_ring._proof_4, zsmul_neg' := int.comm_ring._proof_5, add_left_neg := int.add_left_neg, add_comm := int.add_comm, mul := int.mul, mul_assoc := int.mul_assoc, one := int.one, one_mul := int.one_mul, mul_one := int.mul_one, npow := ring.npow._default int.one int.mul int.one_mul int.mul_one, npow_zero' := int.comm_ring._proof_6, npow_succ' := int.comm_ring._proof_7, left_distrib := int.distrib_left, right_distrib := int.distrib_right, mul_comm := int.mul_comm}

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]

def int.add_comm_monoid :

add_comm_monoid ℤ

Equations

int.add_comm_monoid = add_comm_group.to_add_comm_monoid ℤ

@[protected, instance]

def int.add_monoid :

Equations

int.add_monoid = sub_neg_monoid.to_add_monoid ℤ

@[protected, instance]

def int.monoid :

Equations

int.monoid = ring.to_monoid ℤ

@[protected, instance]

def int.comm_monoid :

comm_monoid ℤ

Equations

int.comm_monoid = comm_ring.to_comm_monoid ℤ

@[protected, instance]

def int.comm_semigroup :

comm_semigroup ℤ

Equations

int.comm_semigroup = comm_monoid.to_comm_semigroup ℤ

@[protected, instance]

def int.semigroup :

Equations

int.semigroup = semigroup_with_zero.to_semigroup ℤ

@[protected, instance]

def int.add_comm_group :

add_comm_group ℤ

Equations

int.add_comm_group = ring.to_add_comm_group ℤ

@[protected, instance]

def int.add_group :

Equations

int.add_group = add_comm_group.to_add_group ℤ

@[protected, instance]

def int.add_comm_semigroup :

add_comm_semigroup ℤ

Equations

int.add_comm_semigroup = add_comm_monoid.to_add_comm_semigroup ℤ

@[protected, instance]

def int.add_semigroup :

add_semigroup ℤ

Equations

int.add_semigroup = add_monoid.to_add_semigroup ℤ

@[protected, instance]

def int.comm_semiring :

comm_semiring ℤ

Equations

int.comm_semiring = comm_ring.to_comm_semiring

@[protected, instance]

def int.semiring :

Equations

int.semiring = ring.to_semiring

@[protected, instance]

def int.ring :

Equations

int.ring = comm_ring.to_ring ℤ

@[protected, instance]

def int.distrib :

Equations

int.distrib = ring.to_distrib ℤ

@[protected, instance]

def int.linear_ordered_comm_ring :

linear_ordered_comm_ring ℤ

Equations

int.linear_ordered_comm_ring = {add := comm_ring.add int.comm_ring, add_assoc := _, zero := comm_ring.zero int.comm_ring, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul int.comm_ring, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg int.comm_ring, sub := comm_ring.sub int.comm_ring, sub_eq_add_neg := _, zsmul := comm_ring.zsmul int.comm_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := comm_ring.mul int.comm_ring, mul_assoc := _, one := comm_ring.one int.comm_ring, one_mul := _, mul_one := _, npow := comm_ring.npow int.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := linear_order.le int.linear_order, lt := linear_order.lt int.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := int.add_le_add_left, zero_le_one := int.linear_ordered_comm_ring._proof_1, mul_pos := int.mul_pos, le_total := _, decidable_le := linear_order.decidable_le int.linear_order, decidable_eq := linear_order.decidable_eq int.linear_order, decidable_lt := linear_order.decidable_lt int.linear_order, max := max int.linear_order, max_def := _, min := min int.linear_order, min_def := _, exists_pair_ne := _, mul_comm := _}

@[protected, instance]

def int.linear_ordered_add_comm_group :

linear_ordered_add_comm_group ℤ

Equations

int.linear_ordered_add_comm_group = linear_ordered_ring.to_linear_ordered_add_comm_group

@[simp]

theorem int.add_neg_one (i : ℤ) :

i + -1 = i - 1

theorem int.abs_eq_nat_abs (a : ℤ) :

|a| = ↑(a.nat_abs)

theorem int.nat_abs_abs (a : ℤ) :

|a|.nat_abs = a.nat_abs

theorem int.sign_mul_abs (a : ℤ) :

(a.sign) * |a| = a

@[simp]

theorem int.default_eq_zero :

@[protected, instance]

meta def int.has_to_format :

has_to_format ℤ

@[protected, instance]

meta def int.has_reflect :

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 : ℕ) :

0 ≤ -[1+ n] ↔ false

@[simp]

theorem int.neg_succ_not_pos (n : ℕ) :

0 < -[1+ n] ↔ false

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

@[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 : ℕ) :

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

a.succ = a + 1

def int.pred (a : ℤ) :

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

Equations

a.pred = a - 1

theorem int.nat_succ_eq_int_succ (n : ℕ) :

↑(n.succ) = ↑n.succ

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 : ℕ) :

↑(n.succ).pred = ↑n

theorem int.neg_nat_succ (n : ℕ) :

-↑(n.succ) = (-↑n).pred

theorem int.succ_neg_nat_succ (n : ℕ) :

(-↑(n.succ)).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.abs_lt_one_iff {a : ℤ} :

|a| < 1 ↔ a = 0

theorem int.abs_le_one_iff {a : ℤ} :

|a| ≤ 1 ↔ a = 0 ∨ a = 1 ∨ a = -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

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

z.induction_on' b H0 Hs Hp = _.mpr (int.rec (λ (n : ℕ), nat.rec (_.mpr H0) (λ (n : ℕ) (ih : C (int.of_nat n + b)), _.mpr (Hs (int.of_nat n + b) _ ih)) n) (λ (n : ℕ), nat.rec (_.mpr (Hp b _ H0)) (λ (n : ℕ) (ih : C (-[1+ n] + b)), _.mpr (Hp (-[1+ n] + b) _ ih)) n) (z - b))

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

theorem int.nat_abs_add_le (a b : ℤ) :

(a + b).nat_abs ≤ a.nat_abs + b.nat_abs

theorem int.nat_abs_sub_le (a b : ℤ) :

(a - b).nat_abs ≤ a.nat_abs + b.nat_abs

theorem int.nat_abs_neg_of_nat (n : ℕ) :

(int.neg_of_nat n).nat_abs = 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 : ℕ) :

-[1+ m] = -↑m - 1

theorem int.nat_abs_ne_zero_of_ne_zero {z : ℤ} (hz : z ≠ 0) :

z.nat_abs ≠ 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) :

a.nat_abs < b.nat_abs

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.eq_nat_abs_iff_mul_eq_zero {a : ℤ} {n : ℕ} :

a.nat_abs = n ↔ (a - ↑n) * (a + ↑n) = 0

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_le_iff_mul_self_le {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 : ℤ} :

a.nat_abs ∣ b.nat_abs ↔ a ∣ b

theorem int.nat_abs_inj_of_nonneg_of_nonneg {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) :

a.nat_abs = b.nat_abs ↔ a = b

theorem int.nat_abs_inj_of_nonpos_of_nonpos {a b : ℤ} (ha : a ≤ 0) (hb : b ≤ 0) :

a.nat_abs = b.nat_abs ↔ a = b

theorem int.nat_abs_inj_of_nonneg_of_nonpos {a b : ℤ} (ha : 0 ≤ a) (hb : b ≤ 0) :

a.nat_abs = b.nat_abs ↔ a = -b

theorem int.nat_abs_inj_of_nonpos_of_nonneg {a b : ℤ} (ha : a ≤ 0) (hb : 0 ≤ b) :

a.nat_abs = b.nat_abs ↔ -a = b

theorem int.strict_mono_on_nat_abs :

strict_mono_on int.nat_abs (set.Ici 0)

theorem int.strict_anti_on_nat_abs :

strict_anti_on int.nat_abs (set.Iic 0)

theorem int.inj_on_nat_abs_Ici :

set.inj_on int.nat_abs (set.Ici 0)

theorem int.inj_on_nat_abs_Iic :

set.inj_on int.nat_abs (set.Iic 0)

`/` #

@[simp]

theorem int.of_nat_div (m n : ℕ) :

int.of_nat (m / n) = int.of_nat m / int.of_nat 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

@[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) :

-[1+ m] % 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 ≠ 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|

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)

@[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 : ℤ} :

↑n ∣ z ↔ n ∣ z.nat_abs

theorem int.coe_nat_dvd_right {n : ℕ} {z : ℤ} :

z ∣ ↑n ↔ z.nat_abs ∣ n

theorem int.dvd_antisymm {a b : ℤ} (H1 : 0 ≤ a) (H2 : 0 ≤ b) :

a ∣ b → b ∣ a → a = 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 ∣ 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]

def int.decidable_dvd :

decidable_rel has_dvd.dvd

Equations

int.decidable_dvd = λ (a n : ℤ), decidable_of_decidable_of_iff (int.decidable_eq (n % a) 0) _

@[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 ∣ 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.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) :

z.sign.nat_abs = 1

theorem int.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

@[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) :

theorem int.dvd_nat_abs_of_of_nat_dvd {a : ℕ} {z : ℤ} (haz : ↑a ∣ z) :

a ∣ z.nat_abs

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) :

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) :

int.of_nat m + -[1+ n] = -[1+ n - m]

theorem int.of_nat_add_neg_succ_of_nat_of_ge {m n : ℕ} (h : n.succ ≤ m) :

int.of_nat m + -[1+ n] = int.of_nat (m - n.succ)

@[simp]

theorem int.neg_add_neg (m n : ℕ) :

-[1+ m] + -[1+ n] = -[1+ (m + n).succ]

theorem int.nat_abs_le_of_dvd_ne_zero {s t : ℤ} (hst : s ∣ t) (ht : t ≠ 0) :

s.nat_abs ≤ t.nat_abs

theorem int.nat_abs_eq_of_dvd_dvd {s t : ℤ} (hst : s ∣ t) (hts : t ∣ s) :

s.nat_abs = t.nat_abs

theorem int.div_dvd_of_dvd {s t : ℤ} (hst : s ∣ t) :

t / s ∣ t

theorem int.dvd_div_of_mul_dvd {a b c : ℤ} (h : a * b ∣ c) :

b ∣ c / a

to_nat #

theorem int.to_nat_eq_max (a : ℤ) :

↑(a.to_nat) = max a 0

@[simp]

theorem int.to_nat_zero :

@[simp]

theorem int.to_nat_one :

@[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 : ℕ) :

↑n.to_nat = n

@[simp]

theorem int.to_nat_coe_nat_add_one {n : ℕ} :

(↑n + 1).to_nat = n + 1

theorem int.le_to_nat (a : ℤ) :

a ≤ ↑(a.to_nat)

@[simp]

theorem int.to_nat_le {a : ℤ} {n : ℕ} :

a.to_nat ≤ n ↔ 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) :

n ≤ z.to_nat ↔ ↑n ≤ z

@[simp]

theorem int.coe_nat_nonpos_iff {n : ℕ} :

↑n ≤ 0 ↔ n = 0

theorem int.to_nat_le_to_nat {a b : ℤ} (h : a ≤ b) :

a.to_nat ≤ b.to_nat

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

@[simp]

theorem int.to_nat_add_to_nat_neg_eq_nat_abs (n : ℤ) :

n.to_nat + (-n).to_nat = n.nat_abs

def int.to_nat' :

ℤ → option ℕ

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

Equations

-[1+ n].to_nat' = none
↑n.to_nat' = some n

theorem int.mem_to_nat' (a : ℤ) (n : ℕ) :

n ∈ a.to_nat' ↔ a = ↑n

theorem int.to_nat_of_nonpos {z : ℤ} :

z ≤ 0 → z.to_nat = 0

@[simp]

theorem int.to_nat_neg_nat (n : ℕ) :

(-↑n).to_nat = 0

@[simp]

theorem int.to_nat_eq_zero {n : ℤ} :

n.to_nat = 0 ↔ n ≤ 0

units #

@[simp]

theorem int.units_nat_abs (u : ℤ ˣ) :

↑u.nat_abs = 1

theorem int.units_eq_one_or (u : ℤ ˣ) :

u = 1 ∨ u = -1

theorem int.is_unit_eq_one_or {a : ℤ} :

is_unit a → a = 1 ∨ a = -1

theorem int.is_unit_iff {a : ℤ} :

is_unit a ↔ a = 1 ∨ a = -1

theorem int.is_unit_iff_nat_abs_eq {n : ℤ} :

is_unit n ↔ n.nat_abs = 1

theorem int.is_unit_iff_abs_eq {x : ℤ} :

is_unit x ↔ |x| = 1

@[norm_cast]

theorem int.of_nat_is_unit {n : ℕ} :

is_unit ↑n ↔ is_unit n

theorem int.units_inv_eq_self (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 : ℕ) :

↑n.bodd = n.bodd

@[simp]

theorem int.bodd_sub_nat_nat (m n : ℕ) :

(int.sub_nat_nat m n).bodd = bxor m.bodd n.bodd

@[simp]

theorem int.bodd_neg_of_nat (n : ℕ) :

(int.neg_of_nat n).bodd = n.bodd

@[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 : ℤ) :

int.bit b n = 2 * n + cond b 1 0

theorem int.bit_decomp (n : ℤ) :

int.bit n.bodd 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

n.bit_cases_on h = _.mpr (h n.bodd n.div2)

@[simp]

theorem int.bit_zero :

int.bit ff 0 = 0

@[simp]

theorem int.bit_coe_nat (b : bool) (n : ℕ) :

int.bit b ↑n = ↑(nat.bit b n)

@[simp]

theorem int.bit_neg_succ (b : bool) (n : ℕ) :

int.bit b -[1+ n] = -[1+ nat.bit (!b) n]

@[simp]

theorem int.bodd_bit (b : bool) (n : ℤ) :

(int.bit b n).bodd = b

@[simp]

theorem int.bodd_bit0 (n : ℤ) :

(bit0 n).bodd = ff

@[simp]

theorem int.bodd_bit1 (n : ℤ) :

(bit1 n).bodd = tt

@[simp]

theorem int.div2_bit (b : bool) (n : ℤ) :

(int.bit b n).div2 = n

theorem int.bit0_ne_bit1 (m n : ℤ) :

bit0 m ≠ bit1 n

theorem int.bit1_ne_bit0 (m n : ℤ) :

bit1 m ≠ bit0 n

theorem int.bit1_ne_zero (m : ℤ) :

@[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 : ℤ) :

(int.bit b n).test_bit m.succ = n.test_bit m

theorem int.bitwise_or :

int.bitwise bor = int.lor

theorem int.bitwise_and :

int.bitwise band = int.land

theorem int.bitwise_diff :

int.bitwise (λ (a b : bool), a && !b) = int.ldiff

theorem int.bitwise_xor :

int.bitwise bxor = int.lxor

@[simp]

theorem int.bitwise_bit (f : bool → bool → bool) (a : bool) (m : ℤ) (b : bool) (n : ℤ) :

int.bitwise f (int.bit a m) (int.bit b n) = int.bit (f a b) (int.bitwise f 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 → bool → bool) (m n : ℤ) (k : ℕ) :

(int.bitwise f 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 : ℕ) :

(m.ldiff n).test_bit k = m.test_bit k && !n.test_bit 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 : ℕ) :

n.lnot.test_bit k = !n.test_bit 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 : ℕ) :

↑m.shiftl ↑n = ↑(m.shiftl n)

@[simp]

theorem int.shiftr_coe_nat (m n : ℕ) :

↑m.shiftr ↑n = ↑(m.shiftr n)

@[simp]

theorem int.shiftl_neg_succ (m n : ℕ) :

-[1+ m].shiftl ↑n = -[1+ nat.shiftl' tt m n]

@[simp]

theorem int.shiftr_neg_succ (m n : ℕ) :

-[1+ m].shiftr ↑n = -[1+ m.shiftr n]

theorem int.shiftr_add (m : ℤ) (n k : ℕ) :

m.shiftr (↑n + ↑k) = (m.shiftr ↑n).shiftr ↑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

theorem int.eq_zero_of_abs_lt_dvd {m x : ℤ} (h1 : m ∣ x) (h2 : |x| < m) :

x = 0