Nat.pow

Results on the power operation on natural numbers.

pow

theorem Nat.pow_le_pow_left {n : ℕ} {m : ℕ} (h : n ≤ m) (i : ℕ) : n ^ i ≤ m ^ i

Alias of Nat.pow_le_pow_of_le_left.

theorem Nat.pow_le_pow_right {n : ℕ} (hx : n > 0) {i : ℕ} {j : ℕ} : i ≤ j → n ^ i ≤ n ^ j

Alias of Nat.pow_le_pow_of_le_right.

theorem Nat.pow_lt_pow_left {n : ℕ} {x : ℕ} {y : ℕ} (h : x < y) (hn : n ≠ 0) : x ^ n < y ^ n

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₀ : n ≠ 0) (h₁ : 1 < m) : 1 < m ^ n

theorem Nat.two_pow_pos (n : ℕ) : 0 < 2 ^ n

theorem Nat.two_pow_succ (n : ℕ) : 2 ^ (n + 1) = 2 ^ n + 2 ^ n

theorem Nat.one_lt_pow' (n : ℕ) (m : ℕ) : 1 < (m + 2) ^ (n + 1)

@[simp]

theorem Nat.one_lt_pow_iff {k : ℕ} {n : ℕ} (h : k ≠ 0) : 1 < n ^ k ↔ 1 < n

theorem Nat.one_lt_two_pow (n : ℕ) (h₀ : n ≠ 0) : 1 < 2 ^ n

theorem Nat.one_lt_two_pow' (n : ℕ) : 1 < 2 ^ (n + 1)

theorem Nat.pow_right_injective {x : ℕ} (hx : 2 ≤ x) : Function.Injective fun (x_1 : ℕ) => x ^ x_1

theorem Nat.pow_left_strictMono {n : ℕ} (hn : n ≠ 0) : StrictMono fun (x : ℕ) => x ^ n

See also pow_left_strictMonoOn.

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 : n ≠ 0) {f : ℕ → ℕ} (hf : StrictMono f) : StrictMono fun (m : ℕ) => f m ^ n

theorem Nat.pow_le_pow_iff_left {m : ℕ} {x : ℕ} {y : ℕ} (hm : m ≠ 0) : x ^ m ≤ y ^ m ↔ x ≤ y

theorem Nat.pow_lt_pow_iff_left {m : ℕ} {x : ℕ} {y : ℕ} (hm : m ≠ 0) : x ^ m < y ^ m ↔ x < y

theorem Nat.pow_left_injective {m : ℕ} (hm : m ≠ 0) : 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

Deprecated lemmas

Those lemmas have been deprecated on 2023-12-23.

@[deprecated Nat.pow_lt_pow_left]

theorem Nat.pow_lt_pow_of_lt_left {n : ℕ} {x : ℕ} {y : ℕ} (h : x < y) (hn : n ≠ 0) : x ^ n < y ^ n

Alias of Nat.pow_lt_pow_left.

@[deprecated Nat.pow_le_pow_iff_left]

theorem Nat.pow_le_iff_le_left {m : ℕ} {x : ℕ} {y : ℕ} (hm : m ≠ 0) : x ^ m ≤ y ^ m ↔ x ≤ y

Alias of Nat.pow_le_pow_iff_left.

@[deprecated pow_lt_pow_right]

theorem Nat.pow_lt_pow_of_lt_right {R : Type u_3} [StrictOrderedSemiring R] {a : R} {n : ℕ} {m : ℕ} (h : 1 < a) (hmn : m < n) : a ^ m < a ^ n

Alias of pow_lt_pow_right.

@[deprecated pow_right_strictMono]

theorem Nat.pow_right_strictMono {R : Type u_3} [StrictOrderedSemiring R] {a : R} (h : 1 < a) : StrictMono fun (x : ℕ) => a ^ x

Alias of pow_right_strictMono.

---

See also pow_right_strictMono'.

@[deprecated pow_le_pow_iff_right]

theorem Nat.pow_le_iff_le_right {R : Type u_3} [StrictOrderedSemiring R] {a : R} {n : ℕ} {m : ℕ} (h : 1 < a) : a ^ n ≤ a ^ m ↔ n ≤ m

Alias of pow_le_pow_iff_right.

@[deprecated pow_lt_pow_iff_right]

theorem Nat.pow_lt_iff_lt_right {R : Type u_3} [StrictOrderedSemiring R] {a : R} {n : ℕ} {m : ℕ} (h : 1 < a) : a ^ n < a ^ m ↔ n < m

Alias of pow_lt_pow_iff_right.