Documentation

Mathlib.Algebra.Order.Ring.Basic

Basic lemmas about ordered rings #

source
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
source
@[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
source
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)
source
theorem zero_pow_le_one {R : Type u_3} [OrderedSemiring R] (n : ℕ) :
0 ^ n ≤ 1
source
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
source
theorem pow_le_one {R : Type u_3} [OrderedSemiring R] {a : R} (n : ℕ) :
0 ≤ a → a ≤ 1 → a ^ n ≤ 1
source
theorem pow_lt_one {R : Type u_3} [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_3} [OrderedSemiring R] {a : R} (H : 1 ≤ a) (n : ℕ) :
1 ≤ a ^ n
source
theorem pow_right_mono {R : Type u_3} [OrderedSemiring R] {a : R} (h : 1 ≤ a) :
Monotone fun (x : ℕ) => a ^ x
source
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
source
theorem le_self_pow {R : Type u_3} [OrderedSemiring R] {a : R} {m : ℕ} (ha : 1 ≤ a) (h : m ≠ 0) :
a ≤ a ^ m
source
theorem Bound.le_self_pow_of_pos {R : Type u_3} [OrderedSemiring R] {a : R} {m : ℕ} (ha : 1 ≤ a) (h : 0 < m) :
a ≤ a ^ m

The bound tactic can't handle m ≠ 0 goals yet, so we express as 0 < m

source
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
source
theorem one_lt_pow {R : Type u_3} [OrderedSemiring R] {a : R} (ha : 1 < a) {n : ℕ} :
n ≠ 0 → 1 < a ^ n
source
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
source
theorem Bound.pow_le_pow_right_of_le_one_or_one_le {R : Type u_3} [OrderedSemiring R] {a : R} {n : ℕ} {m : ℕ} (h : 1 ≤ a ∧ n ≤ m ∨ 0 ≤ a ∧ a ≤ 1 ∧ m ≤ n) :
a ^ n ≤ a ^ m

bound lemma for branching on 1 ≤ a ∨ a ≤ 1 when proving a ^ n ≤ a ^ m

source
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
source
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.

source
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'.

source
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
source
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
source
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
source
theorem lt_self_pow {R : Type u_3} [StrictOrderedSemiring R] {a : R} {m : ℕ} (h : 1 < a) (hm : 1 < m) :
a < a ^ m
source
theorem pow_right_strictAnti {R : Type u_3} [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_3} [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_3} [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_3} [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_3} [StrictOrderedSemiring R] {a : R} (ha : 0 < a) :
0 < a ^ 2
source
theorem sq_pos_of_neg {R : Type u_3} [StrictOrderedRing R] {a : R} (ha : a < 0) :
0 < a ^ 2
source
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
source
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
source
@[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
source
theorem pow_right_injective {R : Type u_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [LinearOrderedSemiring R] {a : R} (ha : 0 ≤ a) :
a ^ 2 ≤ 1 ↔ a ≤ 1
source
theorem sq_lt_one_iff {R : Type u_3} [LinearOrderedSemiring R] {a : R} (ha : 0 ≤ a) :
a ^ 2 < 1 ↔ a < 1
source
theorem one_le_sq_iff {R : Type u_3} [LinearOrderedSemiring R] {a : R} (ha : 0 ≤ a) :
1 ≤ a ^ 2 ↔ 1 ≤ a
source
theorem one_lt_sq_iff {R : Type u_3} [LinearOrderedSemiring R] {a : R} (ha : 0 ≤ a) :
1 < a ^ 2 ↔ 1 < a
source
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
source
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
source
@[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
source
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

Lemmas for canonically linear ordered semirings or linear ordered rings #

The slightly unusual typeclass assumptions [LinearOrderedSemiring R] [ExistsAddOfLE R] cover two more familiar settings:

source
theorem add_sq_le {R : Type u_3} [LinearOrderedSemiring R] {a : R} {b : R} [ExistsAddOfLE R] :
(a + b) ^ 2 ≤ 2 * (a ^ 2 + b ^ 2)
source
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)
source
theorem Even.add_pow_le {R : Type u_3} [LinearOrderedSemiring R] {a : R} {b : R} {n : ℕ} [ExistsAddOfLE R] (hn : Even n) :
(a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n)
source
theorem Even.pow_nonneg {R : Type u_3} [LinearOrderedSemiring R] {n : ℕ} [ExistsAddOfLE R] (hn : Even n) (a : R) :
0 ≤ a ^ n
source
theorem Even.pow_pos {R : Type u_3} [LinearOrderedSemiring R] {a : R} {n : ℕ} [ExistsAddOfLE R] (hn : Even n) (ha : a ≠ 0) :
0 < a ^ n
source
theorem Even.pow_pos_iff {R : Type u_3} [LinearOrderedSemiring R] {a : R} {n : ℕ} [ExistsAddOfLE R] (hn : Even n) (h₀ : n ≠ 0) :
0 < a ^ n ↔ a ≠ 0
source
theorem Odd.pow_neg_iff {R : Type u_3} [LinearOrderedSemiring R] {a : R} {n : ℕ} [ExistsAddOfLE R] (hn : Odd n) :
a ^ n < 0 ↔ a < 0
source
theorem Odd.pow_nonneg_iff {R : Type u_3} [LinearOrderedSemiring R] {a : R} {n : ℕ} [ExistsAddOfLE R] (hn : Odd n) :
0 ≤ a ^ n ↔ 0 ≤ a
source
theorem Odd.pow_nonpos_iff {R : Type u_3} [LinearOrderedSemiring R] {a : R} {n : ℕ} [ExistsAddOfLE R] (hn : Odd n) :
a ^ n ≤ 0 ↔ a ≤ 0
source
theorem Odd.pow_pos_iff {R : Type u_3} [LinearOrderedSemiring R] {a : R} {n : ℕ} [ExistsAddOfLE R] (hn : Odd n) :
0 < a ^ n ↔ 0 < a
source
theorem Odd.pow_nonpos {R : Type u_3} [LinearOrderedSemiring R] {a : R} {n : ℕ} [ExistsAddOfLE R] (hn : Odd n) :
a ≤ 0 → a ^ n ≤ 0

Alias of the reverse direction of Odd.pow_nonpos_iff.

source
theorem Odd.pow_neg {R : Type u_3} [LinearOrderedSemiring R] {a : R} {n : ℕ} [ExistsAddOfLE R] (hn : Odd n) :
a < 0 → a ^ n < 0

Alias of the reverse direction of Odd.pow_neg_iff.

source
theorem Odd.strictMono_pow {R : Type u_3} [LinearOrderedSemiring R] {n : ℕ} [ExistsAddOfLE R] (hn : Odd n) :
StrictMono fun (a : R) => a ^ n
source
theorem sq_pos_iff {R : Type u_3} [LinearOrderedSemiring R] [ExistsAddOfLE R] {a : R} :
0 < a ^ 2 ↔ a ≠ 0
source
theorem sq_pos_of_ne_zero {R : Type u_3} [LinearOrderedSemiring R] [ExistsAddOfLE R] {a : R} :
a ≠ 0 → 0 < a ^ 2

Alias of the reverse direction of sq_pos_iff.

source
theorem pow_two_pos_of_ne_zero {R : Type u_3} [LinearOrderedSemiring R] [ExistsAddOfLE R] {a : R} :
a ≠ 0 → 0 < a ^ 2

Alias of the reverse direction of sq_pos_iff.

Alias of the reverse direction of sq_pos_iff.

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

Deprecated lemmas #

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

source
@[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.

source
@[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.

source
@[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.

source
@[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.

source
@[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.

source
@[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'.

source
@[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.

source
@[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.

source
@[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.

source
@[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.

source
@[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.

source
@[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.

source
@[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.

source
@[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.

source
@[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.

source
@[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.

source
@[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.

source
@[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'.

source
@[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.

source
@[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.