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 #

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.le_self_pow {n : ℕ} (hn : n ≠ 0) (m : ℕ) :
m ≤ m ^ n
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.pow_mod (a b n : ℕ) :
a ^ b % n = (a % n) ^ b % n
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)
source
theorem nat.lt_of_pow_dvd_right {p i n : ℕ} (hn : n ≠ 0) (hp : 2 ≤ p) (h : p ^ i ∣ n) :
i < n