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 y : R) :
f (x - y) = f (y - x)
theorem pow_add_pow_le {R : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] {x y : R} {n : } (hx : 0 x) (hy : 0 y) (hn : n 0) :
x ^ n + y ^ n (x + y) ^ n
theorem pow_add_pow_le' {R : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] {a b : R} {n : } (ha : 0 a) (hb : 0 b) :
a ^ n + b ^ n 2 * (a + b) ^ n
theorem sq_pos_of_neg {R : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] {a : R} (ha : a < 0) :
0 < a ^ 2
def IsNonarchimedean {R : Type u_3} [LinearOrder R] {α : Type u_4} [Add α] (f : αR) :

A function f : α → R is nonarchimedean if it satisfies the ultrametric inequality f (a + b) ≤ max (f a) (f b) for all a b : α.

Equations
Instances For

    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} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a b : R} [ExistsAddOfLE R] :
    (a + b) ^ 2 2 * (a ^ 2 + b ^ 2)
    theorem add_pow_le {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a 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} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a 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} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {n : } [ExistsAddOfLE R] (hn : Even n) (a : R) :
    0 a ^ n
    theorem Even.pow_pos {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : } [ExistsAddOfLE R] (hn : Even n) (ha : a 0) :
    0 < a ^ n
    theorem Even.pow_pos_iff {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing 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} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : } [ExistsAddOfLE R] (hn : Odd n) :
    a ^ n < 0 a < 0
    theorem Odd.pow_nonneg_iff {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : } [ExistsAddOfLE R] (hn : Odd n) :
    0 a ^ n 0 a
    theorem Odd.pow_nonpos_iff {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : } [ExistsAddOfLE R] (hn : Odd n) :
    a ^ n 0 a 0
    theorem Odd.pow_pos_iff {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : } [ExistsAddOfLE R] (hn : Odd n) :
    0 < a ^ n 0 < a
    theorem Odd.pow_nonpos {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing 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} [Semiring R] [LinearOrder R] [IsStrictOrderedRing 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} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {n : } [ExistsAddOfLE R] (hn : Odd n) :
    StrictMono fun (a : R) => a ^ n
    theorem Odd.pow_injective {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {n : } (hn : Odd n) :
    Function.Injective fun (x : R) => x ^ n
    theorem Odd.pow_lt_pow {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {n : } (hn : Odd n) {a b : R} :
    a ^ n < b ^ n a < b
    theorem Odd.pow_le_pow {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {n : } (hn : Odd n) {a b : R} :
    a ^ n b ^ n a b
    theorem Odd.pow_inj {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {n : } (hn : Odd n) {a b : R} :
    a ^ n = b ^ n a = b
    theorem sq_pos_iff {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {a : R} :
    0 < a ^ 2 a 0
    theorem sq_pos_of_ne_zero {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing 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} [Semiring R] [LinearOrder R] [IsStrictOrderedRing 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} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a b : R} [ExistsAddOfLE R] (h : a ^ 2 b) :
    a ^ 4 b ^ 2