Documentation

Init.Grind.Ordered.Ring

source
class Lean.Grind.OrderedRing (R : Type u) [Semiring R] [LE R] [LT R] [Std.IsPreorder R] extends Lean.Grind.OrderedAdd R :
Prop

A ring which is also equipped with a preorder is considered a strict ordered ring if addition, negation, and multiplication are compatible with the preorder, and 0 < 1.

  • add_le_left_iff {a b : R} (c : R) : a ≤ b ↔ a + c ≤ b + c
  • zero_lt_one : 0 < 1

    In a strict ordered semiring, we have 0 < 1.

  • mul_lt_mul_of_pos_left {a b c : R} : a < b → 0 < c → c * a < c * b

    In a strict ordered semiring, we can multiply an inequality a < b on the left by a positive element 0 < c to obtain c * a < c * b.

  • mul_lt_mul_of_pos_right {a b c : R} : a < b → 0 < c → a * c < b * c

    In a strict ordered semiring, we can multiply an inequality a < b on the right by a positive element 0 < c to obtain a * c < b * c.

Instances
    source
    theorem Lean.Grind.OrderedRing.neg_one_lt_zero {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsPreorder R] [OrderedRing R] :
    -1 < 0
    source
    theorem Lean.Grind.OrderedRing.ofNat_nonneg {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsPreorder R] [OrderedRing R] (x : Nat) :
    OfNat.ofNat x ≥ 0
    source
    theorem Lean.Grind.OrderedRing.le_of_natCast_le_natCast {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsPreorder R] [OrderedRing R] (a b : Nat) :
    ↑a ≤ ↑b → a ≤ b
    source
    theorem Lean.Grind.OrderedRing.le_of_intCast_le_intCast {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsPreorder R] [OrderedRing R] (a b : Int) :
    ↑a ≤ ↑b → a ≤ b
    source
    theorem Lean.Grind.OrderedRing.lt_of_natCast_lt_natCast {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsPreorder R] [OrderedRing R] (a b : Nat) :
    ↑a < ↑b → a < b
    source
    theorem Lean.Grind.OrderedRing.lt_of_intCast_lt_intCast {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsPreorder R] [OrderedRing R] (a b : Int) :
    ↑a < ↑b → a < b
    source
    theorem Lean.Grind.OrderedRing.natCast_le_natCast_of_le {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsPreorder R] [OrderedRing R] (a b : Nat) :
    a ≤ b → ↑a ≤ ↑b
    source
    theorem Lean.Grind.OrderedRing.natCast_nonneg {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsPreorder R] [OrderedRing R] {a : Nat} :
    0 ≤ ↑a
    source
    theorem Lean.Grind.OrderedRing.natCast_lt_natCast_of_lt {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsPreorder R] [OrderedRing R] (a b : Nat) :
    a < b → ↑a < ↑b
    source
    theorem Lean.Grind.OrderedRing.pos_natCast_of_pos {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsPreorder R] [OrderedRing R] (a : Nat) :
    0 < a → 0 < ↑a
    source
    theorem Lean.Grind.OrderedRing.pos_intCast_of_pos {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsPreorder R] [OrderedRing R] (a : Int) :
    0 < a → 0 < ↑a
    source
    theorem Lean.Grind.OrderedRing.neg_intCast_of_neg {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsPreorder R] [OrderedRing R] (a : Int) :
    a < 0 → ↑a < 0
    source
    theorem Lean.Grind.OrderedRing.nonneg_intCast_of_nonneg {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsPreorder R] [OrderedRing R] (a : Int) :
    0 ≤ a → 0 ≤ ↑a
    source
    theorem Lean.Grind.OrderedRing.nonpos_intCast_of_nonpos {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsPreorder R] [OrderedRing R] (a : Int) :
    a ≤ 0 → ↑a ≤ 0
    source
    instance Lean.Grind.OrderedRing.instIsCharPOfNatNatOfLawfulOrderLT {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsPreorder R] [OrderedRing R] :
    IsCharP R 0
    source
    theorem Lean.Grind.OrderedRing.mul_pos {R : Type u} [Ring R] [LE R] [LT R] [Std.IsPreorder R] [OrderedRing R] {a b : R} (h₁ : 0 < a) (h₂ : 0 < b) :
    0 < a * b
    source
    theorem Lean.Grind.OrderedRing.zero_le_one {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsPreorder R] [OrderedRing R] :
    0 ≤ 1
    source
    theorem Lean.Grind.OrderedRing.not_one_lt_zero {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsPreorder R] [OrderedRing R] :
    ¬1 < 0
    source
    theorem Lean.Grind.OrderedRing.mul_le_mul_of_nonneg_left {R : Type u} [Ring R] [LE R] [LT R] [Std.IsPartialOrder R] [OrderedRing R] [Std.LawfulOrderLT R] {a b c : R} (h : a ≤ b) (h' : 0 ≤ c) :
    c * a ≤ c * b
    source
    theorem Lean.Grind.OrderedRing.mul_le_mul_of_nonneg_right {R : Type u} [Ring R] [LE R] [LT R] [Std.IsPartialOrder R] [OrderedRing R] [Std.LawfulOrderLT R] {a b c : R} (h : a ≤ b) (h' : 0 ≤ c) :
    a * c ≤ b * c
    source
    theorem Lean.Grind.OrderedRing.mul_le_mul_of_nonpos_left {R : Type u} [Ring R] [LE R] [LT R] [Std.IsPartialOrder R] [OrderedRing R] [Std.LawfulOrderLT R] {a b c : R} (h : a ≤ b) (h' : c ≤ 0) :
    c * b ≤ c * a
    source
    theorem Lean.Grind.OrderedRing.mul_le_mul_of_nonpos_right {R : Type u} [Ring R] [LE R] [LT R] [Std.IsPartialOrder R] [OrderedRing R] [Std.LawfulOrderLT R] {a b c : R} (h : a ≤ b) (h' : c ≤ 0) :
    b * c ≤ a * c
    source
    theorem Lean.Grind.OrderedRing.mul_lt_mul_of_neg_left {R : Type u} [Ring R] [LE R] [LT R] [Std.IsPartialOrder R] [OrderedRing R] [Std.LawfulOrderLT R] {a b c : R} (h : a < b) (h' : c < 0) :
    c * b < c * a
    source
    theorem Lean.Grind.OrderedRing.mul_lt_mul_of_neg_right {R : Type u} [Ring R] [LE R] [LT R] [Std.IsPartialOrder R] [OrderedRing R] [Std.LawfulOrderLT R] {a b c : R} (h : a < b) (h' : c < 0) :
    b * c < a * c
    source
    theorem Lean.Grind.OrderedRing.mul_nonneg {R : Type u} [Ring R] [LE R] [LT R] [Std.IsPartialOrder R] [OrderedRing R] [Std.LawfulOrderLT R] {a b : R} (h₁ : 0 ≤ a) (h₂ : 0 ≤ b) :
    0 ≤ a * b
    source
    theorem Lean.Grind.OrderedRing.mul_nonneg_of_nonpos_of_nonpos {R : Type u} [Ring R] [LE R] [LT R] [Std.IsPartialOrder R] [OrderedRing R] [Std.LawfulOrderLT R] {a b : R} (h₁ : a ≤ 0) (h₂ : b ≤ 0) :
    0 ≤ a * b
    source
    theorem Lean.Grind.OrderedRing.mul_nonpos_of_nonneg_of_nonpos {R : Type u} [Ring R] [LE R] [LT R] [Std.IsPartialOrder R] [OrderedRing R] [Std.LawfulOrderLT R] {a b : R} (h₁ : 0 ≤ a) (h₂ : b ≤ 0) :
    a * b ≤ 0
    source
    theorem Lean.Grind.OrderedRing.mul_nonpos_of_nonpos_of_nonneg {R : Type u} [Ring R] [LE R] [LT R] [Std.IsPartialOrder R] [OrderedRing R] [Std.LawfulOrderLT R] {a b : R} (h₁ : a ≤ 0) (h₂ : 0 ≤ b) :
    a * b ≤ 0
    source
    theorem Lean.Grind.OrderedRing.mul_pos_of_neg_of_neg {R : Type u} [Ring R] [LE R] [LT R] [Std.IsPartialOrder R] [OrderedRing R] [Std.LawfulOrderLT R] {a b : R} (h₁ : a < 0) (h₂ : b < 0) :
    0 < a * b
    source
    theorem Lean.Grind.OrderedRing.mul_neg_of_pos_of_neg {R : Type u} [Ring R] [LE R] [LT R] [Std.IsPartialOrder R] [OrderedRing R] [Std.LawfulOrderLT R] {a b : R} (h₁ : 0 < a) (h₂ : b < 0) :
    a * b < 0
    source
    theorem Lean.Grind.OrderedRing.mul_neg_of_neg_of_pos {R : Type u} [Ring R] [LE R] [LT R] [Std.IsPartialOrder R] [OrderedRing R] [Std.LawfulOrderLT R] {a b : R} (h₁ : a < 0) (h₂ : 0 < b) :
    a * b < 0
    source
    theorem Lean.Grind.OrderedRing.mul_nonneg_iff {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] {a b : R} :
    0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
    source
    theorem Lean.Grind.OrderedRing.mul_pos_iff {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] {a b : R} :
    0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
    source
    theorem Lean.Grind.OrderedRing.sq_nonneg {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] {a : R} :
    0 ≤ a ^ 2
    source
    theorem Lean.Grind.OrderedRing.sq_pos {R : Type u} [Ring R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] {a : R} (h : a ≠ 0) :
    0 < a ^ 2