Nat.pow

Results on the power operation on natural numbers.

pow

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_strictMono {x : ℕ} (k : 2 ≤ x) : StrictMono fun 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 fun n => x ^ n

theorem Nat.pow_left_strictMono {m : ℕ} (k : 1 ≤ m) : StrictMono fun 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 StrictMono.nat_pow {n : ℕ} (hn : 1 ≤ n) {f : ℕ → ℕ} (hf : StrictMono f) : StrictMono fun 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 fun 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 ^ Nat.succ w = b * (m / b % b ^ w) + m % b

theorem Nat.pow_dvd_pow_iff_pow_le_pow {k : ℕ} {l : ℕ} {x : ℕ} : 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 : ℕ} : 1 < p → 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