mathlib documentation

data.nat.pow

nat.pow #

Results on the power operation on natural numbers.

pow #

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

source
theorem nat.mod_pow_succ {b : ℕ} (w m : ℕ) :
m % b ^ w.succ = b * (m / b % b ^ w) + m % b
source
theorem nat.pow_dvd_pow_iff_pow_le_pow {k l x : ℕ} (w : 0 < x) :
x ^ k ∣ x ^ l ↔ x ^ k ≤ x ^ l
source
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.

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

shiftl and shiftr #

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

size #

source
@[simp]
theorem nat.size_zero  :
0.size = 0
source
@[simp]
theorem nat.size_bit {b : bool} {n : ℕ} (h : nat.bit b n ≠ 0) :
(nat.bit b n).size = n.size.succ
source
@[simp]
theorem nat.size_bit0 {n : ℕ} (h : n ≠ 0) :
(bit0 n).size = n.size.succ
source
@[simp]
theorem nat.size_bit1 (n : ℕ) :
(bit1 n).size = n.size.succ
source
@[simp]
theorem nat.size_one  :
1.size = 1
source
@[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
source
@[simp]
theorem nat.size_shiftl {m : ℕ} (h : m ≠ 0) (n : ℕ) :
(m.shiftl n).size = m.size + n
source
theorem nat.lt_size_self (n : ℕ) :
n < 2 ^ n.size
source
theorem nat.size_le {m n : ℕ} :
m.size ≤ n ↔ m < 2 ^ n
source
theorem nat.lt_size {m n : ℕ} :
m < n.size ↔ 2 ^ m ≤ n
source
theorem nat.size_pos {n : ℕ} :
0 < n.size ↔ 0 < n
source
theorem nat.size_eq_zero {n : ℕ} :
n.size = 0 ↔ n = 0
source
theorem nat.size_pow {n : ℕ} :
(2 ^ n).size = n + 1
source
theorem nat.size_le_size {m n : ℕ} (h : m ≤ n) :
m.size ≤ n.size