Documentation

Mathlib.Data.Int.Order.Lemmas

Further lemmas about the integers #

The distinction between this file and Data.Int.Order.Basic is not particularly clear. They are separated by now to minimize the porting requirements for tactics during the transition to mathlib4. Now that Algebra.Order.Ring.Rat has been ported, please feel free to reorganize these two files.

nat abs #

theorem Int.natAbs_eq_iff_mul_self_eq {a : } {b : } :
a.natAbs = b.natAbs a * a = b * b
theorem Int.natAbs_lt_iff_mul_self_lt {a : } {b : } :
a.natAbs < b.natAbs a * a < b * b
theorem Int.natAbs_le_iff_mul_self_le {a : } {b : } :
a.natAbs b.natAbs a * a b * b
theorem Int.pow_right_injective {a : } (h : 1 < a.natAbs) :
Function.Injective fun (x : ) => a ^ x

units #

theorem Int.eq_zero_of_abs_lt_dvd {m : } {x : } (h1 : m x) (h2 : |x| < m) :
x = 0