Documentation

Mathlib.Data.Int.Dvd.Pow

Basic lemmas about the divisibility relation in involving powers. #

@[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) :
p m