mathlib documentation

data.nat.pow

nat.pow #

Results on the power operation on natural numbers.

pow #

@[protected]
theorem nat.pow_le_pow_of_le_left {x y : } (H : x y) (i : ) :
x ^ i y ^ i
theorem nat.pow_le_pow_of_le_right {x : } (H : 0 < x) {i j : } (h : i j) :
x ^ i x ^ j
theorem nat.pow_lt_pow_of_lt_left {x y : } (H : x < y) {i : } (h : 0 < i) :
x ^ i < y ^ i
theorem nat.pow_lt_pow_of_lt_right {x : } (H : 1 < x) {i j : } (h : i < j) :
x ^ i < x ^ j
theorem nat.pow_lt_pow_succ {p : } (h : 1 < p) (n : ) :
p ^ n < p ^ (n + 1)
theorem nat.lt_pow_self {p : } (h : 1 < p) (n : ) :
n < p ^ n
theorem nat.lt_two_pow (n : ) :
n < 2 ^ n
theorem nat.one_le_pow (n m : ) (h : 0 < m) :
1 m ^ n
theorem nat.one_le_pow' (n m : ) :
1 (m + 1) ^ n
theorem nat.one_le_two_pow (n : ) :
1 2 ^ n
theorem nat.one_lt_pow (n m : ) (h₀ : 0 < n) (h₁ : 1 < m) :
1 < m ^ n
theorem nat.one_lt_pow' (n m : ) :
1 < (m + 2) ^ (n + 1)
@[simp]
theorem nat.one_lt_pow_iff {k n : } (h : 0 k) :
1 < n ^ k 1 < n
theorem nat.one_lt_two_pow (n : ) (h₀ : 0 < n) :
1 < 2 ^ n
theorem nat.one_lt_two_pow' (n : ) :
1 < 2 ^ (n + 1)
theorem nat.pow_right_strict_mono {x : } (k : 2 x) :
strict_mono (λ (n : ), x ^ n)
theorem nat.pow_le_iff_le_right {x m n : } (k : 2 x) :
x ^ m x ^ n m n
theorem nat.pow_lt_iff_lt_right {x m n : } (k : 2 x) :
x ^ m < x ^ n m < n
theorem nat.pow_right_injective {x : } (k : 2 x) :
function.injective (λ (n : ), x ^ n)
theorem nat.pow_left_strict_mono {m : } (k : 1 m) :
strict_mono (λ (x : ), x ^ m)
theorem nat.mul_lt_mul_pow_succ {n a q : } (a0 : 0 < a) (q1 : 1 < q) :
n * q < a * q ^ (n + 1)
theorem strict_mono.nat_pow {n : } (hn : 1 n) {f : } (hf : strict_mono f) :
strict_mono (λ (m : ), f m ^ n)
theorem nat.pow_le_iff_le_left {m x y : } (k : 1 m) :
x ^ m y ^ m x y
theorem nat.pow_lt_iff_lt_left {m x y : } (k : 1 m) :
x ^ m < y ^ m x < y
theorem nat.pow_left_injective {m : } (k : 1 m) :
function.injective (λ (x : ), x ^ m)
theorem nat.sq_sub_sq (a b : ) :
a ^ 2 - b ^ 2 = (a + b) * (a - b)
theorem nat.pow_two_sub_pow_two (a b : ) :
a ^ 2 - b ^ 2 = (a + b) * (a - b)

Alias of nat.sq_sub_sq.

pow and mod / dvd #

theorem nat.pow_mod (a b n : ) :
a ^ b % n = (a % n) ^ b % n
theorem nat.mod_pow_succ {b : } (w m : ) :
m % b ^ w.succ = b * (m / b % b ^ w) + m % b
theorem nat.pow_dvd_pow_iff_pow_le_pow {k l x : } (w : 0 < x) :
x ^ k x ^ l x ^ k x ^ l
theorem nat.pow_dvd_pow_iff_le_right {x k l : } (w : 1 < x) :
x ^ k x ^ l k l

If 1 < x, then x^k divides x^l if and only if k is at most l.

theorem nat.pow_dvd_pow_iff_le_right' {b k l : } :
(b + 2) ^ k (b + 2) ^ l k l
theorem nat.not_pos_pow_dvd {p k : } (hp : 1 < p) (hk : 1 < k) :
¬p ^ k p
theorem nat.pow_dvd_of_le_of_pow_dvd {p m n k : } (hmn : m n) (hdiv : p ^ n k) :
p ^ m k
theorem nat.dvd_of_pow_dvd {p k m : } (hk : 1 k) (hpk : p ^ k m) :
p m
theorem nat.pow_div {x m n : } (h : n m) (hx : 0 < x) :
x ^ m / x ^ n = x ^ (m - n)
theorem nat.lt_of_pow_dvd_right {p i n : } (hn : n 0) (hp : 2 p) (h : p ^ i n) :
i < n

shiftl and shiftr #

theorem nat.shiftl_eq_mul_pow (m n : ) :
m.shiftl n = m * 2 ^ n
theorem nat.shiftl'_tt_eq_mul_pow (m n : ) :
nat.shiftl' bool.tt m n + 1 = (m + 1) * 2 ^ n
theorem nat.one_shiftl (n : ) :
1.shiftl n = 2 ^ n
@[simp]
theorem nat.zero_shiftl (n : ) :
0.shiftl n = 0
theorem nat.shiftr_eq_div_pow (m n : ) :
m.shiftr n = m / 2 ^ n
@[simp]
theorem nat.zero_shiftr (n : ) :
0.shiftr n = 0
theorem nat.shiftl'_ne_zero_left (b : bool) {m : } (h : m 0) (n : ) :
theorem nat.shiftl'_tt_ne_zero (m : ) {n : } (h : n 0) :

size #

@[simp]
theorem nat.size_zero  :
0.size = 0
@[simp]
theorem nat.size_bit {b : bool} {n : } (h : nat.bit b n 0) :
@[simp]
theorem nat.size_bit0 {n : } (h : n 0) :
@[simp]
theorem nat.size_bit1 (n : ) :
@[simp]
theorem nat.size_one  :
1.size = 1
@[simp]
theorem nat.size_shiftl' {b : bool} {m n : } (h : nat.shiftl' b m n 0) :
(nat.shiftl' b m n).size = m.size + n
@[simp]
theorem nat.size_shiftl {m : } (h : m 0) (n : ) :
(m.shiftl n).size = m.size + n
theorem nat.lt_size_self (n : ) :
n < 2 ^ n.size
theorem nat.size_le {m n : } :
m.size n m < 2 ^ n
theorem nat.lt_size {m n : } :
m < n.size 2 ^ m n
theorem nat.size_pos {n : } :
0 < n.size 0 < n
theorem nat.size_eq_zero {n : } :
n.size = 0 n = 0
theorem nat.size_pow {n : } :
(2 ^ n).size = n + 1
theorem nat.size_le_size {m n : } (h : m n) :