Documentation

Mathlib.Algebra.Order.Ring.Basic

Basic lemmas about ordered rings #

theorem MonoidHom.map_neg_one {M : Type u_2} {R : Type u_3} [Ring R] [Monoid M] [LinearOrder M] [MulLeftMono M] (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] [MulLeftMono M] (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] [MulLeftMono M] (f : R →* M) (x : R) (y : R) :
f (x - y) = f (y - x)
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
@[deprecated mul_le_one₀]
theorem mul_le_one {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} {b : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : a 1) (hb₀ : 0 b) (hb : b 1) :
a * b 1

Alias of mul_le_one₀.

@[deprecated pow_le_one₀]
theorem pow_le_one {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] {n : } :
0 aa 1a ^ n 1

Alias of pow_le_one₀.

@[deprecated pow_lt_one₀]
theorem pow_lt_one {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (h₀ : 0 a) (h₁ : a < 1) {n : } :
n 0a ^ n < 1

Alias of pow_lt_one₀.

@[deprecated one_le_pow₀]
theorem one_le_pow_of_one_le {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : 1 a) {n : } :
1 a ^ n

Alias of one_le_pow₀.

@[deprecated one_lt_pow₀]
theorem one_lt_pow {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : 1 < a) {n : } :
n 01 < a ^ n

Alias of one_lt_pow₀.

@[deprecated pow_right_mono₀]
theorem pow_right_mono {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (h : 1 a) :
Monotone fun (x : ) => a ^ x

Alias of pow_right_mono₀.

@[deprecated pow_le_pow_right₀]
theorem pow_le_pow_right {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} {m : } {n : } [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : 1 a) (hmn : m n) :
a ^ m a ^ n

Alias of pow_le_pow_right₀.

@[deprecated le_self_pow₀]
theorem le_self_pow {M₀ : Type u_1} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} {n : } [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : 1 a) (hn : n 0) :
a a ^ n

Alias of le_self_pow₀.

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

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

@[reducible, inline]

Turn an ordered domain into a strict ordered ring.

Equations
Instances For
    theorem pow_lt_pow_left {R : Type u_3} [StrictOrderedSemiring R] {x : R} {y : R} (h : x < y) (hx : 0 x) {n : } :
    n 0x ^ 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 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 * ba < 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:

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

    Alias of the reverse direction of Odd.pow_nonpos_iff.

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

    Alias of the reverse direction of Odd.pow_neg_iff.

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

    Alias of the reverse direction of sq_pos_iff.

    theorem pow_two_pos_of_ne_zero {R : Type u_3} [LinearOrderedSemiring R] [ExistsAddOfLE R] {a : R} :
    a 00 < a ^ 2

    Alias of the reverse direction of sq_pos_iff.


    Alias of the reverse direction of sq_pos_iff.

    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