Basic lemmas about the divisibility relation in ℤ.

theorem Int.natCast_dvd_natCast {m : ℕ} {n : ℕ} : ↑m ∣ ↑n ↔ m ∣ n

theorem Int.natCast_dvd {n : ℕ} {z : ℤ} : ↑n ∣ z ↔ n ∣ z.natAbs

theorem Int.dvd_natCast {n : ℕ} {z : ℤ} : z ∣ ↑n ↔ z.natAbs ∣ n

@[deprecated Int.natCast_dvd_natCast]

theorem Int.coe_nat_dvd {m : ℕ} {n : ℕ} : ↑m ∣ ↑n ↔ m ∣ n

Alias of Int.natCast_dvd_natCast.

@[deprecated Int.dvd_natCast]

theorem Int.coe_nat_dvd_right {n : ℕ} {z : ℤ} : z ∣ ↑n ↔ z.natAbs ∣ n

Alias of Int.dvd_natCast.

@[deprecated Int.natCast_dvd]

theorem Int.coe_nat_dvd_left {n : ℕ} {z : ℤ} : ↑n ∣ z ↔ n ∣ z.natAbs

Alias of Int.natCast_dvd.