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 ∣ Int.natAbs z

theorem Int.dvd_natCast {n : ℕ} {z : ℤ} : z ∣ ↑n ↔ Int.natAbs z ∣ 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 ↔ Int.natAbs z ∣ n

Alias of Int.dvd_natCast.

@[deprecated Int.natCast_dvd]

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

Alias of Int.natCast_dvd.