Miscellaneous lemmas about the integers #

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

This file contains lemmas about integers, which require further imports than data.int.basic or data.int.order.

source

theorem int.le_coe_nat_sub (m n : ℕ) :

↑m - ↑n ≤ ↑(m - n)

succ and pred #

source

@[simp]

theorem int.succ_coe_nat_pos (n : ℕ) :

0 < ↑n + 1

nat abs #

source

theorem int.nat_abs_eq_iff_sq_eq {a b : ℤ} :

a.nat_abs = b.nat_abs ↔ a ^ 2 = b ^ 2

source

theorem int.nat_abs_lt_iff_sq_lt {a b : ℤ} :

a.nat_abs < b.nat_abs ↔ a ^ 2 < b ^ 2

source

theorem int.nat_abs_le_iff_sq_le {a b : ℤ} :

a.nat_abs ≤ b.nat_abs ↔ a ^ 2 ≤ b ^ 2

source

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

source

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

source

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

source

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

source

theorem int.strict_mono_on_nat_abs :

strict_mono_on int.nat_abs (set.Ici 0)

source

theorem int.strict_anti_on_nat_abs :

strict_anti_on int.nat_abs (set.Iic 0)

source

theorem int.inj_on_nat_abs_Ici :

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

source

theorem int.inj_on_nat_abs_Iic :

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

to_nat #

source

theorem int.to_nat_of_nonpos {z : ℤ} :

z ≤ 0 → z.to_nat = 0

bitwise ops #

This lemma is orphaned from data.int.bitwise as it also requires material from data.int.order.

source

@[simp]

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

(int.bit b n).div2 = n