Documentation

Mathlib.Data.Int.Lemmas

Miscellaneous lemmas about the integers #

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

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

succ and pred #

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

natAbs #

source
theorem Int.natAbs_eq_iff_sq_eq {a b : ℤ} :
a.natAbs = b.natAbs ↔ a ^ 2 = b ^ 2
source
theorem Int.natAbs_lt_iff_sq_lt {a b : ℤ} :
a.natAbs < b.natAbs ↔ a ^ 2 < b ^ 2
source
theorem Int.natAbs_le_iff_sq_le {a b : ℤ} :
a.natAbs ≤ b.natAbs ↔ a ^ 2 ≤ b ^ 2
source
theorem Int.natAbs_inj_of_nonneg_of_nonneg {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) :
a.natAbs = b.natAbs ↔ a = b
source
theorem Int.natAbs_inj_of_nonpos_of_nonpos {a b : ℤ} (ha : a ≤ 0) (hb : b ≤ 0) :
a.natAbs = b.natAbs ↔ a = b
source
theorem Int.natAbs_inj_of_nonneg_of_nonpos {a b : ℤ} (ha : 0 ≤ a) (hb : b ≤ 0) :
a.natAbs = b.natAbs ↔ a = -b
source
theorem Int.natAbs_inj_of_nonpos_of_nonneg {a b : ℤ} (ha : a ≤ 0) (hb : 0 ≤ b) :
a.natAbs = b.natAbs ↔ -a = b
source
theorem Int.natAbs_coe_sub_coe_le_of_le {a b n : ℕ} (a_le_n : a ≤ n) (b_le_n : b ≤ n) :
(↑a - ↑b).natAbs ≤ n

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

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

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

source
theorem Int.strictMonoOn_natAbs :
StrictMonoOn Int.natAbs (Set.Ici 0)
source
theorem Int.strictAntiOn_natAbs :
StrictAntiOn Int.natAbs (Set.Iic 0)
source
theorem Int.injOn_natAbs_Ici :
Set.InjOn Int.natAbs (Set.Ici 0)
source
theorem Int.injOn_natAbs_Iic :
Set.InjOn Int.natAbs (Set.Iic 0)

toNat #

source
theorem Int.toNat_of_nonpos {z : ℤ} :
z ≤ 0 → z.toNat = 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
source
@[deprecated Int.le_natCast_sub (since := "2024-04-02")]
theorem Int.le_coe_nat_sub (m n : ℕ) :
↑m - ↑n ≤ ↑(m - n)

Alias of Int.le_natCast_sub.

source
@[deprecated Int.succ_natCast_pos (since := "2024-04-02")]
theorem Int.succ_coe_nat_pos (n : ℕ) :
0 < ↑n + 1

Alias of Int.succ_natCast_pos.

source
@[deprecated Int.natCast_natAbs (since := "2024-04-02")]
theorem Int.coe_natAbs (n : ℤ) :
↑n.natAbs = |n|

Alias of Int.natCast_natAbs.

source
@[deprecated Int.natCast_eq_zero (since := "2024-04-02")]
theorem Int.coe_nat_eq_zero {n : ℕ} :
↑n = 0 ↔ n = 0

Alias of Int.natCast_eq_zero.

source
@[deprecated Int.natCast_ne_zero (since := "2024-04-02")]
theorem Int.coe_nat_ne_zero {n : ℕ} :
↑n ≠ 0 ↔ n ≠ 0

Alias of Int.natCast_ne_zero.

source
@[deprecated Int.natCast_ne_zero_iff_pos (since := "2024-04-02")]
theorem Int.coe_nat_ne_zero_iff_pos {n : ℕ} :
↑n ≠ 0 ↔ 0 < n

Alias of Int.natCast_ne_zero_iff_pos.

source
@[deprecated Int.abs_natCast (since := "2024-04-02")]
theorem Int.abs_coe_nat (n : ℕ) :
|↑n| = ↑n

Alias of Int.abs_natCast.

source
@[deprecated Int.natCast_nonpos_iff (since := "2024-04-02")]
theorem Int.coe_nat_nonpos_iff {n : ℕ} :
↑n ≤ 0 ↔ n = 0

Alias of Int.natCast_nonpos_iff.

source
theorem Int.ediv_emod_unique' {a b r q : ℤ} (h : b ≠ 0) :
a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < |b|

Like Int.ediv_emod_unique, but permitting negative b.