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.

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 : } :
a.natAbs = b.natAbs a ^ 2 = b ^ 2
theorem Int.natAbs_lt_iff_sq_lt {a : } {b : } :
a.natAbs < b.natAbs a ^ 2 < b ^ 2
theorem Int.natAbs_le_iff_sq_le {a : } {b : } :
a.natAbs b.natAbs a ^ 2 b ^ 2
theorem Int.natAbs_inj_of_nonneg_of_nonneg {a : } {b : } (ha : 0 a) (hb : 0 b) :
a.natAbs = b.natAbs a = b
theorem Int.natAbs_inj_of_nonpos_of_nonpos {a : } {b : } (ha : a 0) (hb : b 0) :
a.natAbs = b.natAbs a = b
theorem Int.natAbs_inj_of_nonneg_of_nonpos {a : } {b : } (ha : 0 a) (hb : b 0) :
a.natAbs = b.natAbs a = -b
theorem Int.natAbs_inj_of_nonpos_of_nonneg {a : } {b : } (ha : a 0) (hb : 0 b) :
a.natAbs = b.natAbs -a = b
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.

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.

toNat #

theorem Int.toNat_of_nonpos {z : } :
z 0z.toNat = 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.bit b n).div2 = 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 : ) :
n.natAbs = |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.