mathlib3 documentation

data.int.order.lemmas

Further lemmas about the integers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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. After data.rat.order has been ported, please feel free to reorganize these two files.

nat abs #

source
theorem int.nat_abs_eq_iff_mul_self_eq {a b : ℤ} :
a.nat_abs = b.nat_abs ↔ a * a = b * b
source
theorem int.eq_nat_abs_iff_mul_eq_zero {a : ℤ} {n : ℕ} :
a.nat_abs = n ↔ (a - ↑n) * (a + ↑n) = 0
source
theorem int.nat_abs_lt_iff_mul_self_lt {a b : ℤ} :
a.nat_abs < b.nat_abs ↔ a * a < b * b
source
theorem int.nat_abs_le_iff_mul_self_le {a b : ℤ} :
a.nat_abs ≤ b.nat_abs ↔ a * a ≤ b * b
source
theorem int.dvd_div_of_mul_dvd {a b c : ℤ} (h : a * b ∣ c) :
b ∣ c / a

units #

source
theorem int.eq_zero_of_abs_lt_dvd {m x : ℤ} (h1 : m ∣ x) (h2 : |x| < m) :
x = 0