Lemmas about the interaction of power operations with order

Note that some lemmas are in Algebra/GroupPower/Lemmas.lean as they import files which depend on this file.

theorem zsmul_pos {α : Type u_1} [OrderedAddCommGroup α] {n : ℤ} {a : α} (ha : 0 < a) (hn : 0 < n) : 0 < n • a

theorem one_lt_zpow' {α : Type u_1} [OrderedCommGroup α] {n : ℤ} {a : α} (ha : 1 < a) (hn : 0 < n) : 1 < a ^ n

theorem zsmul_strictMono_left {α : Type u_1} [OrderedAddCommGroup α] {a : α} (ha : 0 < a) : StrictMono fun (n : ℤ) => n • a

theorem zpow_right_strictMono {α : Type u_1} [OrderedCommGroup α] {a : α} (ha : 1 < a) : StrictMono fun (n : ℤ) => a ^ n

theorem zsmul_mono_left {α : Type u_1} [OrderedAddCommGroup α] {a : α} (ha : 0 ≤ a) : Monotone fun (n : ℤ) => n • a

theorem zpow_mono_right {α : Type u_1} [OrderedCommGroup α] {a : α} (ha : 1 ≤ a) : Monotone fun (n : ℤ) => a ^ n

theorem zsmul_le_zsmul {α : Type u_1} [OrderedAddCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 0 ≤ a) (h : m ≤ n) : m • a ≤ n • a

theorem zpow_le_zpow {α : Type u_1} [OrderedCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 1 ≤ a) (h : m ≤ n) : a ^ m ≤ a ^ n

theorem zsmul_lt_zsmul {α : Type u_1} [OrderedAddCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 0 < a) (h : m < n) : m • a < n • a

theorem zpow_lt_zpow {α : Type u_1} [OrderedCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 1 < a) (h : m < n) : a ^ m < a ^ n

theorem zsmul_le_zsmul_iff {α : Type u_1} [OrderedAddCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 0 < a) : m • a ≤ n • a ↔ m ≤ n

theorem zpow_le_zpow_iff {α : Type u_1} [OrderedCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n

theorem zsmul_lt_zsmul_iff {α : Type u_1} [OrderedAddCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 0 < a) : m • a < n • a ↔ m < n

theorem zpow_lt_zpow_iff {α : Type u_1} [OrderedCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 1 < a) : a ^ m < a ^ n ↔ m < n

theorem zsmul_strictMono_right (α : Type u_1) [OrderedAddCommGroup α] {n : ℤ} (hn : 0 < n) : StrictMono fun (x : α) => n • x

theorem zpow_strictMono_left (α : Type u_1) [OrderedCommGroup α] {n : ℤ} (hn : 0 < n) : StrictMono fun (x : α) => x ^ n

theorem zsmul_mono_right (α : Type u_1) [OrderedAddCommGroup α] {n : ℤ} (hn : 0 ≤ n) : Monotone fun (x : α) => n • x

theorem zpow_mono_left (α : Type u_1) [OrderedCommGroup α] {n : ℤ} (hn : 0 ≤ n) : Monotone fun (x : α) => x ^ n

theorem zsmul_le_zsmul' {α : Type u_1} [OrderedAddCommGroup α] {n : ℤ} {a : α} {b : α} (hn : 0 ≤ n) (h : a ≤ b) : n • a ≤ n • b

theorem zpow_le_zpow' {α : Type u_1} [OrderedCommGroup α] {n : ℤ} {a : α} {b : α} (hn : 0 ≤ n) (h : a ≤ b) : a ^ n ≤ b ^ n

theorem zsmul_lt_zsmul' {α : Type u_1} [OrderedAddCommGroup α] {n : ℤ} {a : α} {b : α} (hn : 0 < n) (h : a < b) : n • a < n • b

theorem zpow_lt_zpow' {α : Type u_1} [OrderedCommGroup α] {n : ℤ} {a : α} {b : α} (hn : 0 < n) (h : a < b) : a ^ n < b ^ n

theorem zsmul_le_zsmul_iff' {α : Type u_1} [LinearOrderedAddCommGroup α] {n : ℤ} {a : α} {b : α} (hn : 0 < n) : n • a ≤ n • b ↔ a ≤ b

theorem zpow_le_zpow_iff' {α : Type u_1} [LinearOrderedCommGroup α] {n : ℤ} {a : α} {b : α} (hn : 0 < n) : a ^ n ≤ b ^ n ↔ a ≤ b

theorem zsmul_lt_zsmul_iff' {α : Type u_1} [LinearOrderedAddCommGroup α] {n : ℤ} {a : α} {b : α} (hn : 0 < n) : n • a < n • b ↔ a < b

theorem zpow_lt_zpow_iff' {α : Type u_1} [LinearOrderedCommGroup α] {n : ℤ} {a : α} {b : α} (hn : 0 < n) : a ^ n < b ^ n ↔ a < b

theorem zsmul_right_injective {α : Type u_1} [LinearOrderedAddCommGroup α] {n : ℤ} (hn : n ≠ 0) : Function.Injective fun (x : α) => n • x

See also smul_right_injective. TODO: provide a NoZeroSMulDivisors instance. We can't do that here because importing that definition would create import cycles.

theorem zpow_left_injective {α : Type u_1} [LinearOrderedCommGroup α] {n : ℤ} (hn : n ≠ 0) : Function.Injective fun (x : α) => x ^ n

theorem zsmul_right_inj {α : Type u_1} [LinearOrderedAddCommGroup α] {n : ℤ} {a : α} {b : α} (hn : n ≠ 0) : n • a = n • b ↔ a = b

theorem zpow_left_inj {α : Type u_1} [LinearOrderedCommGroup α] {n : ℤ} {a : α} {b : α} (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b

theorem zsmul_eq_zsmul_iff' {α : Type u_1} [LinearOrderedAddCommGroup α] {n : ℤ} {a : α} {b : α} (hn : n ≠ 0) : n • a = n • b ↔ a = b

Alias of zsmul_right_inj, for ease of discovery alongside zsmul_le_zsmul_iff' and zsmul_lt_zsmul_iff'.

theorem zpow_eq_zpow_iff' {α : Type u_1} [LinearOrderedCommGroup α] {n : ℤ} {a : α} {b : α} (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b

Alias of zpow_left_inj, for ease of discovery alongside zsmul_le_zsmul_iff' and zsmul_lt_zsmul_iff'.

theorem CanonicallyOrderedCommSemiring.pow_pos {R : Type u_3} [CanonicallyOrderedCommSemiring R] {a : R} (H : 0 < a) (n : ℕ) : 0 < a ^ n

theorem zero_pow_le_one {R : Type u_3} [OrderedSemiring R] (n : ℕ) : 0 ^ n ≤ 1

theorem pow_add_pow_le {R : Type u_3} [OrderedSemiring R] {x : R} {y : R} {n : ℕ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hn : n ≠ 0) : x ^ n + y ^ n ≤ (x + y) ^ n

theorem pow_le_one {R : Type u_3} [OrderedSemiring R] {a : R} (n : ℕ) : 0 ≤ a → a ≤ 1 → a ^ n ≤ 1

theorem pow_lt_one {R : Type u_3} [OrderedSemiring R] {a : R} (h₀ : 0 ≤ a) (h₁ : a < 1) {n : ℕ} : n ≠ 0 → a ^ n < 1

theorem one_le_pow_of_one_le {R : Type u_3} [OrderedSemiring R] {a : R} (H : 1 ≤ a) (n : ℕ) : 1 ≤ a ^ n

theorem pow_right_mono {R : Type u_3} [OrderedSemiring R] {a : R} (h : 1 ≤ a) : Monotone fun (x : ℕ) => a ^ x

theorem pow_le_pow_right {R : Type u_3} [OrderedSemiring R] {a : R} {n : ℕ} {m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m

theorem le_self_pow {R : Type u_3} [OrderedSemiring R] {a : R} {m : ℕ} (ha : 1 ≤ a) (h : m ≠ 0) : a ≤ a ^ m

theorem pow_le_pow_left {R : Type u_3} [OrderedSemiring R] {a : R} {b : R} (ha : 0 ≤ a) (hab : a ≤ b) (n : ℕ) : a ^ n ≤ b ^ n

theorem one_lt_pow {R : Type u_3} [OrderedSemiring R] {a : R} (ha : 1 < a) {n : ℕ} : n ≠ 0 → 1 < a ^ n

theorem pow_add_pow_le' {R : Type u_3} [OrderedSemiring R] {a : R} {b : R} {n : ℕ} (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ n + b ^ n ≤ 2 * (a + b) ^ n

theorem pow_lt_pow_left {R : Type u_3} [StrictOrderedSemiring R] {x : R} {y : R} (h : x < y) (hx : 0 ≤ x) {n : ℕ} : n ≠ 0 → x ^ n < y ^ n

theorem pow_left_strictMonoOn {R : Type u_3} [StrictOrderedSemiring R] {n : ℕ} (hn : n ≠ 0) : StrictMonoOn (fun (x : R) => x ^ n) {a : R | 0 ≤ a}

See also pow_left_strictMono and Nat.pow_left_strictMono.

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

See also pow_right_strictMono'.

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

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

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

theorem lt_self_pow {R : Type u_3} [StrictOrderedSemiring R] {a : R} {m : ℕ} (h : 1 < a) (hm : 1 < m) : a < a ^ m

theorem pow_right_strictAnti {R : Type u_3} [StrictOrderedSemiring R] {a : R} (h₀ : 0 < a) (h₁ : a < 1) : StrictAnti fun (x : ℕ) => a ^ x

theorem pow_lt_pow_iff_right_of_lt_one {R : Type u_3} [StrictOrderedSemiring R] {a : R} {n : ℕ} {m : ℕ} (h₀ : 0 < a) (h₁ : a < 1) : a ^ m < a ^ n ↔ n < m

theorem pow_lt_pow_right_of_lt_one {R : Type u_3} [StrictOrderedSemiring R] {a : R} {n : ℕ} {m : ℕ} (h₀ : 0 < a) (h₁ : a < 1) (hmn : m < n) : a ^ n < a ^ m

theorem pow_lt_self_of_lt_one {R : Type u_3} [StrictOrderedSemiring R] {a : R} {n : ℕ} (h₀ : 0 < a) (h₁ : a < 1) (hn : 1 < n) : a ^ n < a

theorem sq_pos_of_pos {R : Type u_3} [StrictOrderedSemiring R] {a : R} (ha : 0 < a) : 0 < a ^ 2

theorem pow_bit0_pos_of_neg {R : Type u_3} [StrictOrderedRing R] {a : R} (ha : a < 0) (n : ℕ) : 0 < a ^ bit0 n

theorem pow_bit1_neg {R : Type u_3} [StrictOrderedRing R] {a : R} (ha : a < 0) (n : ℕ) : a ^ bit1 n < 0

theorem sq_pos_of_neg {R : Type u_3} [StrictOrderedRing R] {a : R} (ha : a < 0) : 0 < a ^ 2

theorem pow_le_pow_iff_left {R : Type u_3} [LinearOrderedSemiring R] {a : R} {b : R} {n : ℕ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n ≤ b ^ n ↔ a ≤ b

theorem pow_lt_pow_iff_left {R : Type u_3} [LinearOrderedSemiring R] {a : R} {b : R} {n : ℕ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n < b ^ n ↔ a < b

@[simp]

theorem pow_left_inj {R : Type u_3} [LinearOrderedSemiring R] {a : R} {b : R} {n : ℕ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b

theorem pow_right_injective {R : Type u_3} [LinearOrderedSemiring R] {a : R} (ha₀ : 0 < a) (ha₁ : a ≠ 1) : Function.Injective fun (x : ℕ) => a ^ x

@[simp]

theorem pow_right_inj {R : Type u_3} [LinearOrderedSemiring R] {a : R} {m : ℕ} {n : ℕ} (ha₀ : 0 < a) (ha₁ : a ≠ 1) : a ^ m = a ^ n ↔ m = n

theorem pow_le_one_iff_of_nonneg {R : Type u_3} [LinearOrderedSemiring R] {a : R} {n : ℕ} (ha : 0 ≤ a) (hn : n ≠ 0) : a ^ n ≤ 1 ↔ a ≤ 1

theorem one_le_pow_iff_of_nonneg {R : Type u_3} [LinearOrderedSemiring R] {a : R} {n : ℕ} (ha : 0 ≤ a) (hn : n ≠ 0) : 1 ≤ a ^ n ↔ 1 ≤ a

theorem pow_lt_one_iff_of_nonneg {R : Type u_3} [LinearOrderedSemiring R] {a : R} {n : ℕ} (ha : 0 ≤ a) (hn : n ≠ 0) : a ^ n < 1 ↔ a < 1

theorem one_lt_pow_iff_of_nonneg {R : Type u_3} [LinearOrderedSemiring R] {a : R} {n : ℕ} (ha : 0 ≤ a) (hn : n ≠ 0) : 1 < a ^ n ↔ 1 < a

theorem pow_eq_one_iff_of_nonneg {R : Type u_3} [LinearOrderedSemiring R] {a : R} {n : ℕ} (ha : 0 ≤ a) (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1

theorem sq_le_one_iff {R : Type u_3} [LinearOrderedSemiring R] {a : R} (ha : 0 ≤ a) : a ^ 2 ≤ 1 ↔ a ≤ 1

theorem sq_lt_one_iff {R : Type u_3} [LinearOrderedSemiring R] {a : R} (ha : 0 ≤ a) : a ^ 2 < 1 ↔ a < 1

theorem one_le_sq_iff {R : Type u_3} [LinearOrderedSemiring R] {a : R} (ha : 0 ≤ a) : 1 ≤ a ^ 2 ↔ 1 ≤ a

theorem one_lt_sq_iff {R : Type u_3} [LinearOrderedSemiring R] {a : R} (ha : 0 ≤ a) : 1 < a ^ 2 ↔ 1 < a

theorem lt_of_pow_lt_pow_left {R : Type u_3} [LinearOrderedSemiring R] {a : R} {b : R} (n : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) : a < b

theorem le_of_pow_le_pow_left {R : Type u_3} [LinearOrderedSemiring R] {a : R} {b : R} {n : ℕ} (hn : n ≠ 0) (hb : 0 ≤ b) (h : a ^ n ≤ b ^ n) : a ≤ b

@[simp]

theorem sq_eq_sq {R : Type u_3} [LinearOrderedSemiring R] {a : R} {b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 = b ^ 2 ↔ a = b

theorem lt_of_mul_self_lt_mul_self {R : Type u_3} [LinearOrderedSemiring R] {a : R} {b : R} (hb : 0 ≤ b) : a * a < b * b → a < b

theorem add_sq_le {R : Type u_3} [LinearOrderedSemiring R] {a : R} {b : R} [ExistsAddOfLE R] : (a + b) ^ 2 ≤ 2 * (a ^ 2 + b ^ 2)

theorem add_pow_le {R : Type u_3} [LinearOrderedSemiring R] {a : R} {b : R} [ExistsAddOfLE R] (ha : 0 ≤ a) (hb : 0 ≤ b) (n : ℕ) : (a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n)

theorem Even.add_pow_le {R : Type u_3} [LinearOrderedSemiring R] {a : R} {b : R} {n : ℕ} [ExistsAddOfLE R] (hn : ∃ (k : ℕ), 2 * k = n) : (a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n)

theorem pow_bit0_nonneg {R : Type u_3} [LinearOrderedRing R] (a : R) (n : ℕ) : 0 ≤ a ^ bit0 n

theorem pow_bit0_pos {R : Type u_3} [LinearOrderedRing R] {a : R} (h : a ≠ 0) (n : ℕ) : 0 < a ^ bit0 n

theorem sq_pos_of_ne_zero {R : Type u_3} [LinearOrderedRing R] (a : R) (h : a ≠ 0) : 0 < a ^ 2

theorem pow_two_pos_of_ne_zero {R : Type u_3} [LinearOrderedRing R] (a : R) (h : a ≠ 0) : 0 < a ^ 2

Alias of sq_pos_of_ne_zero.

theorem pow_bit0_pos_iff {R : Type u_3} [LinearOrderedRing R] (a : R) {n : ℕ} (hn : n ≠ 0) : 0 < a ^ bit0 n ↔ a ≠ 0

@[simp]

theorem pow_bit1_neg_iff {R : Type u_3} [LinearOrderedRing R] {a : R} {n : ℕ} : a ^ bit1 n < 0 ↔ a < 0

@[simp]

theorem pow_bit1_nonneg_iff {R : Type u_3} [LinearOrderedRing R] {a : R} {n : ℕ} : 0 ≤ a ^ bit1 n ↔ 0 ≤ a

@[simp]

theorem pow_bit1_nonpos_iff {R : Type u_3} [LinearOrderedRing R] {a : R} {n : ℕ} : a ^ bit1 n ≤ 0 ↔ a ≤ 0

@[simp]

theorem pow_bit1_pos_iff {R : Type u_3} [LinearOrderedRing R] {a : R} {n : ℕ} : 0 < a ^ bit1 n ↔ 0 < a

theorem strictMono_pow_bit1 {R : Type u_3} [LinearOrderedRing R] (n : ℕ) : StrictMono fun (x : R) => x ^ bit1 n

theorem sq_pos_iff {R : Type u_3} [LinearOrderedRing R] (a : R) : 0 < a ^ 2 ↔ a ≠ 0

theorem pow_four_le_pow_two_of_pow_two_le {R : Type u_3} [LinearOrderedRing R] {a : R} {b : R} (h : a ^ 2 ≤ b) : a ^ 4 ≤ b ^ 2

theorem MonoidHom.map_neg_one {M : Type u_2} {R : Type u_3} [Ring R] [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] (f : R →* M) : f (-1) = 1

@[simp]

theorem MonoidHom.map_neg {M : Type u_2} {R : Type u_3} [Ring R] [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] (f : R →* M) (x : R) : f (-x) = f x

theorem MonoidHom.map_sub_swap {M : Type u_2} {R : Type u_3} [Ring R] [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] (f : R →* M) (x : R) (y : R) : f (x - y) = f (y - x)

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

See also pow_left_strictMonoOn.

theorem StrictMono.nat_pow {α : Type u_1} {n : ℕ} {f : α → ℕ} [Preorder α] (hn : n ≠ 0) (hf : StrictMono f) : StrictMono fun (x : α) => f x ^ n

Deprecated lemmas

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

@[deprecated pow_right_mono]

theorem pow_mono {R : Type u_3} [OrderedSemiring R] {a : R} (h : 1 ≤ a) : Monotone fun (x : ℕ) => a ^ x

Alias of pow_right_mono.

@[deprecated pow_le_pow_right]

theorem pow_le_pow {R : Type u_3} [OrderedSemiring R] {a : R} {n : ℕ} {m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m

Alias of pow_le_pow_right.

@[deprecated pow_le_pow_left]

theorem pow_le_pow_of_le_left {R : Type u_3} [OrderedSemiring R] {a : R} {b : R} (ha : 0 ≤ a) (hab : a ≤ b) (n : ℕ) : a ^ n ≤ b ^ n

Alias of pow_le_pow_left.

@[deprecated pow_lt_pow_left]

theorem pow_lt_pow_of_lt_left {R : Type u_3} [StrictOrderedSemiring R] {x : R} {y : R} (h : x < y) (hx : 0 ≤ x) {n : ℕ} : n ≠ 0 → x ^ n < y ^ n

Alias of pow_lt_pow_left.

@[deprecated pow_left_strictMonoOn]

theorem strictMonoOn_pow {R : Type u_3} [StrictOrderedSemiring R] {n : ℕ} (hn : n ≠ 0) : StrictMonoOn (fun (x : R) => x ^ n) {a : R | 0 ≤ a}

Alias of pow_left_strictMonoOn.

---

See also pow_left_strictMono and Nat.pow_left_strictMono.

@[deprecated pow_right_strictMono]

theorem pow_strictMono_right {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_lt_pow_right]

theorem pow_lt_pow {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_lt_pow_iff_right]

theorem pow_lt_pow_iff {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.

@[deprecated pow_le_pow_iff_right]

theorem pow_le_pow_iff {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 lt_self_pow]

theorem self_lt_pow {R : Type u_3} [StrictOrderedSemiring R] {a : R} {m : ℕ} (h : 1 < a) (hm : 1 < m) : a < a ^ m

Alias of lt_self_pow.

@[deprecated pow_right_strictAnti]

theorem strictAnti_pow {R : Type u_3} [StrictOrderedSemiring R] {a : R} (h₀ : 0 < a) (h₁ : a < 1) : StrictAnti fun (x : ℕ) => a ^ x

Alias of pow_right_strictAnti.

@[deprecated pow_lt_pow_iff_right_of_lt_one]

theorem pow_lt_pow_iff_of_lt_one {R : Type u_3} [StrictOrderedSemiring R] {a : R} {n : ℕ} {m : ℕ} (h₀ : 0 < a) (h₁ : a < 1) : a ^ m < a ^ n ↔ n < m

Alias of pow_lt_pow_iff_right_of_lt_one.

@[deprecated pow_lt_pow_right_of_lt_one]

theorem pow_lt_pow_of_lt_one {R : Type u_3} [StrictOrderedSemiring R] {a : R} {n : ℕ} {m : ℕ} (h₀ : 0 < a) (h₁ : a < 1) (hmn : m < n) : a ^ n < a ^ m

Alias of pow_lt_pow_right_of_lt_one.

@[deprecated lt_of_pow_lt_pow_left]

theorem lt_of_pow_lt_pow {R : Type u_3} [LinearOrderedSemiring R] {a : R} {b : R} (n : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) : a < b

Alias of lt_of_pow_lt_pow_left.

@[deprecated le_of_pow_le_pow_left]

theorem le_of_pow_le_pow {R : Type u_3} [LinearOrderedSemiring R] {a : R} {b : R} {n : ℕ} (hn : n ≠ 0) (hb : 0 ≤ b) (h : a ^ n ≤ b ^ n) : a ≤ b

Alias of le_of_pow_le_pow_left.

@[deprecated le_self_pow]

theorem self_le_pow {R : Type u_3} [OrderedSemiring R] {a : R} {m : ℕ} (ha : 1 ≤ a) (h : m ≠ 0) : a ≤ a ^ m

Alias of le_self_pow.

@[deprecated Nat.pow_lt_pow_left]

theorem Nat.pow_lt_pow_of_lt_left {a : ℕ} {b : ℕ} (h : a < b) {n : ℕ} : n ≠ 0 → a ^ n < b ^ n

Alias of Nat.pow_lt_pow_left.

@[deprecated Nat.pow_le_pow_iff_left]

theorem Nat.pow_le_iff_le_left {a : ℕ} {b : ℕ} {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ b ^ n ↔ a ≤ b

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.