mathlib documentation

data.int.dvd.basic

Basic lemmas about the divisibility relation in . #

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

@[norm_cast]
theorem int.coe_nat_dvd {m n : } :
m n m n
theorem int.coe_nat_dvd_left {n : } {z : } :
theorem int.coe_nat_dvd_right {n : } {z : } :
theorem int.le_of_dvd {a b : } (bpos : 0 < b) (H : a b) :
a b
theorem int.eq_one_of_dvd_one {a : } (H : 0 a) (H' : a 1) :
a = 1
theorem int.eq_one_of_mul_eq_one_right {a b : } (H : 0 a) (H' : a * b = 1) :
a = 1
theorem int.eq_one_of_mul_eq_one_left {a b : } (H : 0 b) (H' : a * b = 1) :
b = 1
theorem int.of_nat_dvd_of_dvd_nat_abs {a : } {z : } (haz : a z.nat_abs) :
a z
theorem int.dvd_nat_abs_of_of_nat_dvd {a : } {z : } (haz : a z) :
theorem int.dvd_antisymm {a b : } (H1 : 0 a) (H2 : 0 b) :
a b b a a = b