Documentation

Mathlib.Algebra.Order.Ring.Basic

Basic lemmas about ordered rings #

source
theorem IsSquare.nonneg {R : Type u_3} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] {x : R} (h : IsSquare x) :
0 ≤ x
source
@[simp]
theorem not_isSquare_of_neg {R : Type u_3} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] {x : R} (h : x < 0) :
¬IsSquare x
source
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
source
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
source
theorem Even.pow_le_pow_of_nonpos {R : Type u_3} [Ring R] [PartialOrder R] [IsOrderedRing R] {n : ℕ} (hn : Even n) {a b : R} (hb : b ≤ 0) (hab : a ≤ b) :
b ^ n ≤ a ^ n
source
theorem Even.pow_lt_pow_of_nonpos {R : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] {n : ℕ} (hn : Even n) {a b : R} (hb : b ≤ 0) (hab : a < b) (hn₀ : n ≠ 0) :
b ^ n < a ^ n
source
theorem sq_pos_of_neg {R : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] {a : R} (ha : a < 0) :
0 < a ^ 2
source
theorem Even.pow_nonneg {R : Type u_3} [Semiring R] [LinearOrder R] [IsOrderedRing R] [ExistsAddOfLE R] {n : ℕ} (hn : Even n) (a : R) :
0 ≤ a ^ n
source
theorem pow_four_le_pow_two_of_pow_two_le {R : Type u_3} [Semiring R] [LinearOrder R] [IsOrderedRing R] [ExistsAddOfLE R] {a b : R} (h : a ^ 2 ≤ b) :
a ^ 4 ≤ b ^ 2
source
theorem pow_add_pow_eq_zero_iff_of_even {R : Type u_3} [Semiring R] [LinearOrder R] [IsOrderedRing R] [ExistsAddOfLE R] [NoZeroDivisors R] {n : ℕ} (hn : n ≠ 0) (hn' : Even n) (x y : R) :
x ^ n + y ^ n = 0 ↔ x = 0 ∧ y = 0
source
def IsNonarchimedean {R : Type u_3} [LinearOrder R] {α : Type u_4} [Add α] (f : α → R) :
Prop

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 [IsStrictOrderedRing R] [ExistsAddOfLE R] cover two more familiar settings:

    source
    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)
    source
    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)
    source
    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)
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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
    source
    theorem Odd.pow_nonpos {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing 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} [Semiring R] [LinearOrder R] [IsStrictOrderedRing 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} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {n : ℕ} [ExistsAddOfLE R] (hn : Odd n) :
    StrictMono fun (a : R) => a ^ n
    source
    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
    source
    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
    source
    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
    source
    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
    source
    theorem sq_pos_iff {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {a : R} :
    0 < a ^ 2 ↔ a ≠ 0
    source
    theorem sq_pos_of_ne_zero {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing 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} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {a : R} :
    a ≠ 0 → 0 < a ^ 2

    Alias of sq_pos_of_ne_zero.

    Alias of the reverse direction of sq_pos_iff.