mathlib3 documentation

data.int.div

Lemmas relating / in with the ordering. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem int.eq_mul_div_of_mul_eq_mul_of_dvd_left {a b c d : } (hb : b 0) (hbc : b c) (h : b * a = c * d) :
a = c / b * d
theorem int.eq_zero_of_dvd_of_nat_abs_lt_nat_abs {a b : } (w : a b) (h : b.nat_abs < a.nat_abs) :
b = 0

If an integer with larger absolute value divides an integer, it is zero.

theorem int.eq_zero_of_dvd_of_nonneg_of_lt {a b : } (w₁ : 0 a) (w₂ : a < b) (h : b a) :
a = 0
theorem int.eq_of_mod_eq_of_nat_abs_sub_lt_nat_abs {a b c : } (h1 : a % b = c) (h2 : (a - c).nat_abs < b.nat_abs) :
a = c

If two integers are congruent to a sufficiently large modulus, they are equal.

theorem int.nat_abs_le_of_dvd_ne_zero {s t : } (hst : s t) (ht : t 0) :