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 : ℕ} :

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.dvd_antisymm {a b : ℤ} (H1 : 0 ≤ a) (H2 : 0 ≤ b) :

a ∣ b → b ∣ a → a = b

Basic lemmas about the divisibility relation in ℤ. #