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_coe_nat_sub (m : ) (n : ) :
m - n ↑(m - n)

succ and pred #

theorem Int.succ_coe_nat_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_inj_of_nonneg_of_nonneg {a : } {b : } (ha : 0 a) (hb : 0 b) :
theorem Int.natAbs_inj_of_nonpos_of_nonpos {a : } {b : } (ha : a 0) (hb : b 0) :
theorem Int.natAbs_inj_of_nonneg_of_nonpos {a : } {b : } (ha : 0 a) (hb : b 0) :
theorem Int.natAbs_inj_of_nonpos_of_nonneg {a : } {b : } (ha : a 0) (hb : 0 b) :

toNat #

theorem Int.toNat_of_nonpos {z : } :
z 0Int.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 : ) :