mathlib3 documentation

data.nat.pow

nat.pow #

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

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.le_self_pow {n : } (hn : n 0) (m : ) :
m m ^ n
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