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 CanonicallyOrderedCommSemiring.pow_pos {R : Type u_2} [CanonicallyOrderedCommSemiring R] {a : R} (H : 0 < a) (n : ℕ) :

0 < a ^ n

source

theorem zero_pow_le_one {R : Type u_2} [OrderedSemiring R] (n : ℕ) :

0 ^ n ≤ 1

source

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

x ^ n + y ^ n ≤ (x + y) ^ n

source

theorem pow_le_one {R : Type u_2} [OrderedSemiring R] {a : R} (n : ℕ) :

0 ≤ a → a ≤ 1 → a ^ n ≤ 1

source

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

n ≠ 0 → a ^ n < 1

source

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

1 ≤ a ^ n

source

theorem pow_right_mono {R : Type u_2} [OrderedSemiring R] {a : R} (h : 1 ≤ a) :

Monotone fun (x : ℕ) => a ^ x

source

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

a ^ n ≤ a ^ m

source

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

a ≤ a ^ m

source

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

a ^ n ≤ b ^ n

source

theorem one_lt_pow {R : Type u_2} [OrderedSemiring R] {a : R} (ha : 1 < a) {n : ℕ} :

n ≠ 0 → 1 < a ^ n

source

theorem pow_add_pow_le' {R : Type u_2} [OrderedSemiring R] {a : R} {b : R} {n : ℕ} (ha : 0 ≤ a) (hb : 0 ≤ b) :

a ^ n + b ^ n ≤ 2 * (a + b) ^ n

source

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

n ≠ 0 → x ^ n < y ^ n

source

theorem pow_left_strictMonoOn {R : Type u_2} [StrictOrderedSemiring R] {n : ℕ} (hn : n ≠ 0) :

StrictMonoOn (fun (x : R) => x ^ n) (Set.Ici 0)

See also pow_left_strictMono and Nat.pow_left_strictMono.

source

theorem pow_right_strictMono {R : Type u_2} [StrictOrderedSemiring R] {a : R} (h : 1 < a) :

StrictMono fun (x : ℕ) => a ^ x

See also pow_right_strictMono'.

source

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

a ^ m < a ^ n

source

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

a ^ n < a ^ m ↔ n < m

source

theorem pow_le_pow_iff_right {R : Type u_2} [StrictOrderedSemiring R] {a : R} {n : ℕ} {m : ℕ} (h : 1 < a) :

a ^ n ≤ a ^ m ↔ n ≤ m

source

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

a < a ^ m

source

theorem pow_right_strictAnti {R : Type u_2} [StrictOrderedSemiring R] {a : R} (h₀ : 0 < a) (h₁ : a < 1) :

StrictAnti fun (x : ℕ) => a ^ x

source

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

a ^ m < a ^ n ↔ n < m

source

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

a ^ n < a ^ m

source

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

a ^ n < a

source

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

0 < a ^ 2

source

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

0 < a ^ bit0 n

source

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

a ^ bit1 n < 0

source

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

0 < a ^ 2

source

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

a ^ n ≤ b ^ n ↔ a ≤ b

source

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

a ^ n < b ^ n ↔ a < b

source

@[simp]

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

a ^ n = b ^ n ↔ a = b

source

theorem pow_right_injective {R : Type u_2} [LinearOrderedSemiring R] {a : R} (ha₀ : 0 < a) (ha₁ : a ≠ 1) :

Function.Injective fun (x : ℕ) => a ^ x

source

@[simp]

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

a ^ m = a ^ n ↔ m = n

source

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

a ^ n ≤ 1 ↔ a ≤ 1

source

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

1 ≤ a ^ n ↔ 1 ≤ a

source

theorem pow_lt_one_iff_of_nonneg {R : Type u_2} [LinearOrderedSemiring R] {a : R} {n : ℕ} (ha : 0 ≤ a) (hn : n ≠ 0) :

a ^ n < 1 ↔ a < 1

source

theorem one_lt_pow_iff_of_nonneg {R : Type u_2} [LinearOrderedSemiring R] {a : R} {n : ℕ} (ha : 0 ≤ a) (hn : n ≠ 0) :

1 < a ^ n ↔ 1 < a

source

theorem pow_eq_one_iff_of_nonneg {R : Type u_2} [LinearOrderedSemiring R] {a : R} {n : ℕ} (ha : 0 ≤ a) (hn : n ≠ 0) :

a ^ n = 1 ↔ a = 1

source

theorem sq_le_one_iff {R : Type u_2} [LinearOrderedSemiring R] {a : R} (ha : 0 ≤ a) :

a ^ 2 ≤ 1 ↔ a ≤ 1

source

theorem sq_lt_one_iff {R : Type u_2} [LinearOrderedSemiring R] {a : R} (ha : 0 ≤ a) :

a ^ 2 < 1 ↔ a < 1

source

theorem one_le_sq_iff {R : Type u_2} [LinearOrderedSemiring R] {a : R} (ha : 0 ≤ a) :

1 ≤ a ^ 2 ↔ 1 ≤ a

source

theorem one_lt_sq_iff {R : Type u_2} [LinearOrderedSemiring R] {a : R} (ha : 0 ≤ a) :

1 < a ^ 2 ↔ 1 < a

source

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

a < b

source

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

a ≤ b

source

@[simp]

theorem sq_eq_sq {R : Type u_2} [LinearOrderedSemiring R] {a : R} {b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) :

a ^ 2 = b ^ 2 ↔ a = b

source

theorem lt_of_mul_self_lt_mul_self {R : Type u_2} [LinearOrderedSemiring R] {a : R} {b : R} (hb : 0 ≤ b) :

a * a < b * b → a < b

source

theorem pow_abs {R : Type u_2} [LinearOrderedRing R] (a : R) (n : ℕ) :

|a| ^ n = |a ^ n|

source

theorem abs_neg_one_pow {R : Type u_2} [LinearOrderedRing R] (n : ℕ) :

|(-1) ^ n| = 1

source

theorem abs_pow_eq_one {R : Type u_2} [LinearOrderedRing R] (a : R) {n : ℕ} (h : n ≠ 0) :

|a ^ n| = 1 ↔ |a| = 1

source

theorem pow_bit0_nonneg {R : Type u_2} [LinearOrderedRing R] (a : R) (n : ℕ) :

0 ≤ a ^ bit0 n

source

theorem pow_two_nonneg {α : Type u} [LinearOrderedSemiring α] [ExistsAddOfLE α] (a : α) :

0 ≤ a ^ 2

Alias of sq_nonneg.

source

theorem pow_bit0_pos {R : Type u_2} [LinearOrderedRing R] {a : R} (h : a ≠ 0) (n : ℕ) :

0 < a ^ bit0 n

source

theorem sq_pos_of_ne_zero {R : Type u_2} [LinearOrderedRing R] (a : R) (h : a ≠ 0) :

0 < a ^ 2

source

theorem pow_two_pos_of_ne_zero {R : Type u_2} [LinearOrderedRing R] (a : R) (h : a ≠ 0) :

0 < a ^ 2

Alias of sq_pos_of_ne_zero.

source

theorem pow_bit0_pos_iff {R : Type u_2} [LinearOrderedRing R] (a : R) {n : ℕ} (hn : n ≠ 0) :

0 < a ^ bit0 n ↔ a ≠ 0

source

theorem sq_pos_iff {R : Type u_2} [LinearOrderedRing R] (a : R) :

0 < a ^ 2 ↔ a ≠ 0

source

@[simp]

theorem sq_abs {R : Type u_2} [LinearOrderedRing R] (x : R) :

|x| ^ 2 = x ^ 2

source

theorem abs_sq {R : Type u_2} [LinearOrderedRing R] (x : R) :

|x ^ 2| = x ^ 2

source

theorem sq_lt_sq {R : Type u_2} [LinearOrderedRing R] {x : R} {y : R} :

x ^ 2 < y ^ 2 ↔ |x| < |y|

source

theorem sq_lt_sq' {R : Type u_2} [LinearOrderedRing R] {x : R} {y : R} (h1 : -y < x) (h2 : x < y) :

x ^ 2 < y ^ 2

source

theorem sq_le_sq {R : Type u_2} [LinearOrderedRing R] {x : R} {y : R} :

x ^ 2 ≤ y ^ 2 ↔ |x| ≤ |y|

source

theorem sq_le_sq' {R : Type u_2} [LinearOrderedRing R] {x : R} {y : R} (h1 : -y ≤ x) (h2 : x ≤ y) :

x ^ 2 ≤ y ^ 2

source

theorem abs_lt_of_sq_lt_sq {R : Type u_2} [LinearOrderedRing R] {x : R} {y : R} (h : x ^ 2 < y ^ 2) (hy : 0 ≤ y) :

|x| < y

source

theorem abs_lt_of_sq_lt_sq' {R : Type u_2} [LinearOrderedRing R] {x : R} {y : R} (h : x ^ 2 < y ^ 2) (hy : 0 ≤ y) :

-y < x ∧ x < y

source

theorem abs_le_of_sq_le_sq {R : Type u_2} [LinearOrderedRing R] {x : R} {y : R} (h : x ^ 2 ≤ y ^ 2) (hy : 0 ≤ y) :

|x| ≤ y

source

theorem abs_le_of_sq_le_sq' {R : Type u_2} [LinearOrderedRing R] {x : R} {y : R} (h : x ^ 2 ≤ y ^ 2) (hy : 0 ≤ y) :

-y ≤ x ∧ x ≤ y

source

theorem sq_eq_sq_iff_abs_eq_abs {R : Type u_2} [LinearOrderedRing R] (x : R) (y : R) :

x ^ 2 = y ^ 2 ↔ |x| = |y|

source

@[simp]

theorem sq_le_one_iff_abs_le_one {R : Type u_2} [LinearOrderedRing R] (x : R) :

x ^ 2 ≤ 1 ↔ |x| ≤ 1

source

@[simp]

theorem sq_lt_one_iff_abs_lt_one {R : Type u_2} [LinearOrderedRing R] (x : R) :

x ^ 2 < 1 ↔ |x| < 1

source

@[simp]

theorem one_le_sq_iff_one_le_abs {R : Type u_2} [LinearOrderedRing R] (x : R) :

1 ≤ x ^ 2 ↔ 1 ≤ |x|

source

@[simp]

theorem one_lt_sq_iff_one_lt_abs {R : Type u_2} [LinearOrderedRing R] (x : R) :

1 < x ^ 2 ↔ 1 < |x|

source

theorem pow_four_le_pow_two_of_pow_two_le {R : Type u_2} [LinearOrderedRing R] {x : R} {y : R} (h : x ^ 2 ≤ y) :

x ^ 4 ≤ y ^ 2

source

theorem pow_pos_iff {M : Type u_1} [LinearOrderedCommMonoidWithZero M] [NoZeroDivisors M] {a : M} {n : ℕ} (hn : 0 < n) :

0 < a ^ n ↔ 0 < a

source

theorem pow_lt_pow_succ {M : Type u_1} [LinearOrderedCommGroupWithZero M] {a : M} {n : ℕ} (ha : 1 < a) :

a ^ n < a ^ Nat.succ n

source

theorem pow_lt_pow_right₀ {M : Type u_1} [LinearOrderedCommGroupWithZero M] {a : M} {m : ℕ} {n : ℕ} (ha : 1 < a) (hmn : m < n) :

a ^ m < a ^ n

source

theorem MonoidHom.map_neg_one {M : Type u_1} {R : Type u_2} [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

source

@[simp]

theorem MonoidHom.map_neg {M : Type u_1} {R : Type u_2} [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

source

theorem MonoidHom.map_sub_swap {M : Type u_1} {R : Type u_2} [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)