Basic lemmas about the divisibility relation in `ℤ` involving powers. #

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

@[simp]

theorem int.sign_pow_bit1 (k : ℕ) (n : ℤ) :

theorem int.pow_dvd_of_le_of_pow_dvd {p m n : ℕ} {k : ℤ} (hmn : m ≤ n) (hdiv : ↑(p ^ n) ∣ k) :

↑(p ^ m) ∣ k

theorem int.dvd_of_pow_dvd {p k : ℕ} {m : ℤ} (hk : 1 ≤ k) (hpk : ↑(p ^ k) ∣ m) :

Basic lemmas about the divisibility relation in ℤ involving powers. #