Miscellaneous lemmas about the integers

This file contains lemmas about integers, which require further imports than Data.Int.Basic or Data.Int.Order.

theorem Int.le_natCast_sub (m : ℕ) (n : ℕ) : ↑m - ↑n ≤ ↑(m - n)

succ and pred

theorem Int.succ_natCast_pos (n : ℕ) : 0 < ↑n + 1

natAbs

theorem Int.natAbs_eq_iff_sq_eq {a : ℤ} {b : ℤ} : Int.natAbs a = Int.natAbs b ↔ a ^ 2 = b ^ 2

theorem Int.natAbs_lt_iff_sq_lt {a : ℤ} {b : ℤ} : Int.natAbs a < Int.natAbs b ↔ a ^ 2 < b ^ 2

theorem Int.natAbs_le_iff_sq_le {a : ℤ} {b : ℤ} : Int.natAbs a ≤ Int.natAbs b ↔ a ^ 2 ≤ b ^ 2

theorem Int.natAbs_inj_of_nonneg_of_nonneg {a : ℤ} {b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) : Int.natAbs a = Int.natAbs b ↔ a = b

theorem Int.natAbs_inj_of_nonpos_of_nonpos {a : ℤ} {b : ℤ} (ha : a ≤ 0) (hb : b ≤ 0) : Int.natAbs a = Int.natAbs b ↔ a = b

theorem Int.natAbs_inj_of_nonneg_of_nonpos {a : ℤ} {b : ℤ} (ha : 0 ≤ a) (hb : b ≤ 0) : Int.natAbs a = Int.natAbs b ↔ a = -b

theorem Int.natAbs_inj_of_nonpos_of_nonneg {a : ℤ} {b : ℤ} (ha : a ≤ 0) (hb : 0 ≤ b) : Int.natAbs a = Int.natAbs b ↔ -a = b

theorem Int.natAbs_coe_sub_coe_le_of_le {a : ℕ} {b : ℕ} {n : ℕ} (a_le_n : a ≤ n) (b_le_n : b ≤ n) : Int.natAbs (↑a - ↑b) ≤ n

A specialization of abs_sub_le_of_nonneg_of_le for working with the signed subtraction of natural numbers.

theorem Int.natAbs_coe_sub_coe_lt_of_lt {a : ℕ} {b : ℕ} {n : ℕ} (a_lt_n : a < n) (b_lt_n : b < n) : Int.natAbs (↑a - ↑b) < n

A specialization of abs_sub_lt_of_nonneg_of_lt for working with the signed subtraction of natural numbers.

theorem Int.strictMonoOn_natAbs : StrictMonoOn Int.natAbs (Set.Ici 0)

theorem Int.strictAntiOn_natAbs : StrictAntiOn Int.natAbs (Set.Iic 0)

theorem Int.injOn_natAbs_Ici : Set.InjOn Int.natAbs (Set.Ici 0)

theorem Int.injOn_natAbs_Iic : Set.InjOn Int.natAbs (Set.Iic 0)

toNat

theorem Int.toNat_of_nonpos {z : ℤ} : z ≤ 0 → Int.toNat z = 0

bitwise ops

This lemma is orphaned from Data.Int.Bitwise as it also requires material from Data.Int.Order.

@[simp]

theorem Int.div2_bit (b : Bool) (n : ℤ) : Int.div2 (Int.bit b n) = n

@[deprecated Int.le_natCast_sub]

theorem Int.le_coe_nat_sub (m : ℕ) (n : ℕ) : ↑m - ↑n ≤ ↑(m - n)

Alias of Int.le_natCast_sub.

@[deprecated Int.succ_natCast_pos]

theorem Int.succ_coe_nat_pos (n : ℕ) : 0 < ↑n + 1

Alias of Int.succ_natCast_pos.

@[deprecated Int.natCast_natAbs]

theorem Int.coe_natAbs (n : ℤ) : ↑(Int.natAbs n) = |n|

Alias of Int.natCast_natAbs.

@[deprecated Int.natCast_eq_zero]

theorem Int.coe_nat_eq_zero {n : ℕ} : ↑n = 0 ↔ n = 0

Alias of Int.natCast_eq_zero.

@[deprecated Int.natCast_ne_zero]

theorem Int.coe_nat_ne_zero {n : ℕ} : ↑n ≠ 0 ↔ n ≠ 0

Alias of Int.natCast_ne_zero.

@[deprecated Int.natCast_ne_zero_iff_pos]

theorem Int.coe_nat_ne_zero_iff_pos {n : ℕ} : ↑n ≠ 0 ↔ 0 < n

Alias of Int.natCast_ne_zero_iff_pos.

@[deprecated Int.abs_natCast]

theorem Int.abs_coe_nat (n : ℕ) : |↑n| = ↑n

Alias of Int.abs_natCast.

@[deprecated Int.natCast_nonpos_iff]

theorem Int.coe_nat_nonpos_iff {n : ℕ} : ↑n ≤ 0 ↔ n = 0

Alias of Int.natCast_nonpos_iff.