mathlib documentation

algebra.order.ring

Ordered rings and semirings #

This file develops the basics of ordered (semi)rings.

Each typeclass here comprises

For short,

Typeclasses #

and some typeclasses to define ordered rings by specifying their nonegative elements:

Hierarchy #

The hardest part of proving order lemmas might be to figure out the correct generality and its corresponding typeclass. Here's an attempt at demystifying it. For each typeclass, we list its immediate predecessors and what conditions are added to each of them.

TODO #

We're still missing some typeclasses, like

source
theorem add_one_le_two_mul {α : Type u} [preorder α] [semiring α] [covariant_class α α has_add.add has_le.le] {a : α} (a1 : 1 ≤ a) :
a + 1 ≤ 2 * a
source
@[instance]
def ordered_semiring.to_semiring (α : Type u) [self : ordered_semiring α] :
semiring α
source
@[class]
structure ordered_semiring (α : Type u) :
Type u
  • add : α → α → α
  • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • nsmul : ℕ → α → α
  • nsmul_zero' : (∀ (x : α), ordered_semiring.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ℕ) (x : α), ordered_semiring.nsmul n.succ x = x + ordered_semiring.nsmul n x) . "try_refl_tac"
  • add_comm : ∀ (a b : α), a + b = b + a
  • mul : α → α → α
  • left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
  • right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
  • zero_mul : ∀ (a : α), 0 * a = 0
  • mul_zero : ∀ (a : α), a * 0 = 0
  • mul_assoc : ∀ (a b c : α), (a * b) * c = a * b * c
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • npow : ℕ → α → α
  • npow_zero' : (∀ (x : α), ordered_semiring.npow 0 x = 1) . "try_refl_tac"
  • npow_succ' : (∀ (n : ℕ) (x : α), ordered_semiring.npow n.succ x = x * ordered_semiring.npow n x) . "try_refl_tac"
  • add_left_cancel : ∀ (a b c : α), a + b = a + c → b = c
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
  • le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c
  • zero_le_one : 0 ≤ 1
  • mul_lt_mul_of_pos_left : ∀ (a b c : α), a < b → 0 < c → c * a < c * b
  • mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b → 0 < c → a * c < b * c

An ordered_semiring α is a semiring α with a partial order such that addition is monotone and multiplication by a positive number is strictly monotone.

Instances
source
@[instance]
def ordered_semiring.to_ordered_cancel_add_comm_monoid (α : Type u) [self : ordered_semiring α] :
ordered_cancel_add_comm_monoid α
source
@[simp]
theorem zero_le_one {α : Type u} [ordered_semiring α] :
0 ≤ 1
source
theorem zero_le_two {α : Type u} [ordered_semiring α] :
0 ≤ 2
source
theorem one_le_two {α : Type u} [ordered_semiring α] :
1 ≤ 2
source
@[simp]
theorem zero_lt_one {α : Type u} [ordered_semiring α] [nontrivial α] :
0 < 1
source
theorem zero_lt_two {α : Type u} [ordered_semiring α] [nontrivial α] :
0 < 2
source
theorem two_ne_zero {α : Type u} [ordered_semiring α] [nontrivial α] :
2 ≠ 0
source
theorem one_lt_two {α : Type u} [ordered_semiring α] [nontrivial α] :
1 < 2
source
theorem zero_lt_three {α : Type u} [ordered_semiring α] [nontrivial α] :
0 < 3
source
theorem zero_lt_four {α : Type u} [ordered_semiring α] [nontrivial α] :
0 < 4
source
theorem mul_lt_mul_of_pos_left {α : Type u} [ordered_semiring α] {a b c : α} (h₁ : a < b) (h₂ : 0 < c) :
c * a < c * b
source
theorem mul_lt_mul_of_pos_right {α : Type u} [ordered_semiring α] {a b c : α} (h₁ : a < b) (h₂ : 0 < c) :
a * c < b * c
source
@[protected]
theorem decidable.mul_le_mul_of_nonneg_left {α : Type u} [ordered_semiring α] {a b c : α} [decidable_rel has_le.le] (h₁ : a ≤ b) (h₂ : 0 ≤ c) :
c * a ≤ c * b
source
theorem mul_le_mul_of_nonneg_left {α : Type u} [ordered_semiring α] {a b c : α} :
a ≤ b → 0 ≤ c → c * a ≤ c * b
source
@[protected]
theorem decidable.mul_le_mul_of_nonneg_right {α : Type u} [ordered_semiring α] {a b c : α} [decidable_rel has_le.le] (h₁ : a ≤ b) (h₂ : 0 ≤ c) :
a * c ≤ b * c
source
theorem mul_le_mul_of_nonneg_right {α : Type u} [ordered_semiring α] {a b c : α} :
a ≤ b → 0 ≤ c → a * c ≤ b * c
source
@[protected]
theorem decidable.mul_le_mul {α : Type u} [ordered_semiring α] {a b c d : α} [decidable_rel has_le.le] (hac : a ≤ c) (hbd : b ≤ d) (nn_b : 0 ≤ b) (nn_c : 0 ≤ c) :
a * b ≤ c * d
source
theorem mul_le_mul {α : Type u} [ordered_semiring α] {a b c d : α} :
a ≤ c → b ≤ d → 0 ≤ b → 0 ≤ c → a * b ≤ c * d
source
@[protected]
theorem decidable.mul_nonneg_le_one_le {α : Type u_1} [ordered_semiring α] [decidable_rel has_le.le] {a b c : α} (h₁ : 0 ≤ c) (h₂ : a ≤ c) (h₃ : 0 ≤ b) (h₄ : b ≤ 1) :
a * b ≤ c
source
theorem mul_nonneg_le_one_le {α : Type u_1} [ordered_semiring α] {a b c : α} :
0 ≤ c → a ≤ c → 0 ≤ b → b ≤ 1 → a * b ≤ c
source
@[protected]
theorem decidable.mul_nonneg {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (ha : 0 ≤ a) (hb : 0 ≤ b) :
0 ≤ a * b
source
theorem mul_nonneg {α : Type u} [ordered_semiring α] {a b : α} :
0 ≤ a → 0 ≤ b → 0 ≤ a * b
source
@[protected]
theorem decidable.mul_nonpos_of_nonneg_of_nonpos {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (ha : 0 ≤ a) (hb : b ≤ 0) :
a * b ≤ 0
source
theorem mul_nonpos_of_nonneg_of_nonpos {α : Type u} [ordered_semiring α] {a b : α} :
0 ≤ a → b ≤ 0 → a * b ≤ 0
source
@[protected]
theorem decidable.mul_nonpos_of_nonpos_of_nonneg {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (ha : a ≤ 0) (hb : 0 ≤ b) :
a * b ≤ 0
source
theorem mul_nonpos_of_nonpos_of_nonneg {α : Type u} [ordered_semiring α] {a b : α} :
a ≤ 0 → 0 ≤ b → a * b ≤ 0
source
@[protected]
theorem decidable.mul_lt_mul {α : Type u} [ordered_semiring α] {a b c d : α} [decidable_rel has_le.le] (hac : a < c) (hbd : b ≤ d) (pos_b : 0 < b) (nn_c : 0 ≤ c) :
a * b < c * d
source
theorem mul_lt_mul {α : Type u} [ordered_semiring α] {a b c d : α} :
a < c → b ≤ d → 0 < b → 0 ≤ c → a * b < c * d
source
@[protected]
theorem decidable.mul_lt_mul' {α : Type u} [ordered_semiring α] {a b c d : α} [decidable_rel has_le.le] (h1 : a ≤ c) (h2 : b < d) (h3 : 0 ≤ b) (h4 : 0 < c) :
a * b < c * d
source
theorem mul_lt_mul' {α : Type u} [ordered_semiring α] {a b c d : α} :
a ≤ c → b < d → 0 ≤ b → 0 < c → a * b < c * d
source
theorem mul_pos {α : Type u} [ordered_semiring α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
0 < a * b
source
theorem mul_neg_of_pos_of_neg {α : Type u} [ordered_semiring α] {a b : α} (ha : 0 < a) (hb : b < 0) :
a * b < 0
source
theorem mul_neg_of_neg_of_pos {α : Type u} [ordered_semiring α] {a b : α} (ha : a < 0) (hb : 0 < b) :
a * b < 0
source
@[protected]
theorem decidable.mul_self_lt_mul_self {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (h1 : 0 ≤ a) (h2 : a < b) :
a * a < b * b
source
theorem mul_self_lt_mul_self {α : Type u} [ordered_semiring α] {a b : α} (h1 : 0 ≤ a) (h2 : a < b) :
a * a < b * b
source
@[protected]
theorem decidable.strict_mono_on_mul_self {α : Type u} [ordered_semiring α] [decidable_rel has_le.le] :
strict_mono_on (λ (x : α), x * x) (set.Ici 0)
source
theorem strict_mono_on_mul_self {α : Type u} [ordered_semiring α] :
strict_mono_on (λ (x : α), x * x) (set.Ici 0)
source
@[protected]
theorem decidable.mul_self_le_mul_self {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (h1 : 0 ≤ a) (h2 : a ≤ b) :
a * a ≤ b * b
source
theorem mul_self_le_mul_self {α : Type u} [ordered_semiring α] {a b : α} (h1 : 0 ≤ a) (h2 : a ≤ b) :
a * a ≤ b * b
source
@[protected]
theorem decidable.mul_lt_mul'' {α : Type u} [ordered_semiring α] {a b c d : α} [decidable_rel has_le.le] (h1 : a < c) (h2 : b < d) (h3 : 0 ≤ a) (h4 : 0 ≤ b) :
a * b < c * d
source
theorem mul_lt_mul'' {α : Type u} [ordered_semiring α] {a b c d : α} :
a < c → b < d → 0 ≤ a → 0 ≤ b → a * b < c * d
source
@[protected]
theorem decidable.le_mul_of_one_le_right {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (hb : 0 ≤ b) (h : 1 ≤ a) :
b ≤ b * a
source
theorem le_mul_of_one_le_right {α : Type u} [ordered_semiring α] {a b : α} :
0 ≤ b → 1 ≤ a → b ≤ b * a
source
@[protected]
theorem decidable.le_mul_of_one_le_left {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (hb : 0 ≤ b) (h : 1 ≤ a) :
b ≤ a * b
source
theorem le_mul_of_one_le_left {α : Type u} [ordered_semiring α] {a b : α} :
0 ≤ b → 1 ≤ a → b ≤ a * b
source
@[protected]
theorem decidable.lt_mul_of_one_lt_right {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (hb : 0 < b) (h : 1 < a) :
b < b * a
source
theorem lt_mul_of_one_lt_right {α : Type u} [ordered_semiring α] {a b : α} :
0 < b → 1 < a → b < b * a
source
@[protected]
theorem decidable.lt_mul_of_one_lt_left {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (hb : 0 < b) (h : 1 < a) :
b < a * b
source
theorem lt_mul_of_one_lt_left {α : Type u} [ordered_semiring α] {a b : α} :
0 < b → 1 < a → b < a * b
source
@[protected]
theorem decidable.add_le_mul_two_add {α : Type u} [ordered_semiring α] [decidable_rel has_le.le] {a b : α} (a2 : 2 ≤ a) (b0 : 0 ≤ b) :
a + (2 + b) ≤ a * (2 + b)
source
theorem add_le_mul_two_add {α : Type u} [ordered_semiring α] {a b : α} :
2 ≤ a → 0 ≤ b → a + (2 + b) ≤ a * (2 + b)
source
@[protected]
theorem decidable.one_le_mul_of_one_le_of_one_le {α : Type u} [ordered_semiring α] [decidable_rel has_le.le] {a b : α} (a1 : 1 ≤ a) (b1 : 1 ≤ b) :
1 ≤ a * b
source
theorem one_le_mul_of_one_le_of_one_le {α : Type u} [ordered_semiring α] {a b : α} :
1 ≤ a → 1 ≤ b → 1 ≤ a * b
source
def function.injective.ordered_semiring {α : Type u} [ordered_semiring α] {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :
ordered_semiring β

Pullback an ordered_semiring under an injective map. See note [reducible non-instances].

Equations
source
theorem bit1_pos {α : Type u} [ordered_semiring α] {a : α} [nontrivial α] (h : 0 ≤ a) :
0 < bit1 a
source
theorem lt_add_one {α : Type u} [ordered_semiring α] [nontrivial α] (a : α) :
a < a + 1
source
theorem lt_one_add {α : Type u} [ordered_semiring α] [nontrivial α] (a : α) :
a < 1 + a
source
theorem bit1_pos' {α : Type u} [ordered_semiring α] {a : α} (h : 0 < a) :
0 < bit1 a
source
@[protected]
theorem decidable.one_lt_mul {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (ha : 1 ≤ a) (hb : 1 < b) :
1 < a * b
source
theorem one_lt_mul {α : Type u} [ordered_semiring α] {a b : α} :
1 ≤ a → 1 < b → 1 < a * b
source
@[protected]
theorem decidable.mul_le_one {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (ha : a ≤ 1) (hb' : 0 ≤ b) (hb : b ≤ 1) :
a * b ≤ 1
source
theorem mul_le_one {α : Type u} [ordered_semiring α] {a b : α} :
a ≤ 1 → 0 ≤ b → b ≤ 1 → a * b ≤ 1
source
@[protected]
theorem decidable.one_lt_mul_of_le_of_lt {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (ha : 1 ≤ a) (hb : 1 < b) :
1 < a * b
source
theorem one_lt_mul_of_le_of_lt {α : Type u} [ordered_semiring α] {a b : α} :
1 ≤ a → 1 < b → 1 < a * b
source
@[protected]
theorem decidable.one_lt_mul_of_lt_of_le {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (ha : 1 < a) (hb : 1 ≤ b) :
1 < a * b
source
theorem one_lt_mul_of_lt_of_le {α : Type u} [ordered_semiring α] {a b : α} :
1 < a → 1 ≤ b → 1 < a * b
source
@[protected]
theorem decidable.mul_le_of_le_one_right {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (ha : 0 ≤ a) (hb1 : b ≤ 1) :
a * b ≤ a
source
theorem mul_le_of_le_one_right {α : Type u} [ordered_semiring α] {a b : α} :
0 ≤ a → b ≤ 1 → a * b ≤ a
source
@[protected]
theorem decidable.mul_le_of_le_one_left {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (hb : 0 ≤ b) (ha1 : a ≤ 1) :
a * b ≤ b
source
theorem mul_le_of_le_one_left {α : Type u} [ordered_semiring α] {a b : α} :
0 ≤ b → a ≤ 1 → a * b ≤ b
source
@[protected]
theorem decidable.mul_lt_one_of_nonneg_of_lt_one_left {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (ha0 : 0 ≤ a) (ha : a < 1) (hb : b ≤ 1) :
a * b < 1
source
theorem mul_lt_one_of_nonneg_of_lt_one_left {α : Type u} [ordered_semiring α] {a b : α} :
0 ≤ a → a < 1 → b ≤ 1 → a * b < 1
source
@[protected]
theorem decidable.mul_lt_one_of_nonneg_of_lt_one_right {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (ha : a ≤ 1) (hb0 : 0 ≤ b) (hb : b < 1) :
a * b < 1
source
theorem mul_lt_one_of_nonneg_of_lt_one_right {α : Type u} [ordered_semiring α] {a b : α} :
a ≤ 1 → 0 ≤ b → b < 1 → a * b < 1
source
@[instance]
def ordered_comm_semiring.to_comm_semiring (α : Type u) [self : ordered_comm_semiring α] :
comm_semiring α
source
@[instance]
def ordered_comm_semiring.to_ordered_semiring (α : Type u) [self : ordered_comm_semiring α] :
ordered_semiring α
source
@[class]
structure ordered_comm_semiring (α : Type u) :
Type u
  • add : α → α → α
  • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • nsmul : ℕ → α → α
  • nsmul_zero' : (∀ (x : α), ordered_comm_semiring.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ℕ) (x : α), ordered_comm_semiring.nsmul n.succ x = x + ordered_comm_semiring.nsmul n x) . "try_refl_tac"
  • add_comm : ∀ (a b : α), a + b = b + a
  • mul : α → α → α
  • left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
  • right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
  • zero_mul : ∀ (a : α), 0 * a = 0
  • mul_zero : ∀ (a : α), a * 0 = 0
  • mul_assoc : ∀ (a b c : α), (a * b) * c = a * b * c
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • npow : ℕ → α → α
  • npow_zero' : (∀ (x : α), ordered_comm_semiring.npow 0 x = 1) . "try_refl_tac"
  • npow_succ' : (∀ (n : ℕ) (x : α), ordered_comm_semiring.npow n.succ x = x * ordered_comm_semiring.npow n x) . "try_refl_tac"
  • add_left_cancel : ∀ (a b c : α), a + b = a + c → b = c
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
  • le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c
  • zero_le_one : 0 ≤ 1
  • mul_lt_mul_of_pos_left : ∀ (a b c : α), a < b → 0 < c → c * a < c * b
  • mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b → 0 < c → a * c < b * c
  • mul_comm : ∀ (a b : α), a * b = b * a

An ordered_comm_semiring α is a commutative semiring α with a partial order such that addition is monotone and multiplication by a positive number is strictly monotone.

Instances
source
def function.injective.ordered_comm_semiring {α : Type u} [ordered_comm_semiring α] {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :
ordered_comm_semiring β

Pullback an ordered_comm_semiring under an injective map. See note [reducible non-instances].

Equations
source
@[instance]
def linear_ordered_semiring.to_ordered_semiring (α : Type u) [self : linear_ordered_semiring α] :
ordered_semiring α
source
@[class]
structure linear_ordered_semiring (α : Type u) :
Type u

A linear_ordered_semiring α is a nontrivial semiring α with a linear order such that addition is monotone and multiplication by a positive number is strictly monotone.

Instances
source
@[instance]
def linear_ordered_semiring.to_linear_ordered_add_comm_monoid (α : Type u) [self : linear_ordered_semiring α] :
linear_ordered_add_comm_monoid α
source
@[instance]
def linear_ordered_semiring.to_nontrivial (α : Type u) [self : linear_ordered_semiring α] :
nontrivial α
source
theorem zero_lt_one' {α : Type u} [linear_ordered_semiring α] :
0 < 1
source
theorem lt_of_mul_lt_mul_left {α : Type u} [linear_ordered_semiring α] {a b c : α} (h : c * a < c * b) (hc : 0 ≤ c) :
a < b
source
theorem lt_of_mul_lt_mul_right {α : Type u} [linear_ordered_semiring α] {a b c : α} (h : a * c < b * c) (hc : 0 ≤ c) :
a < b
source
theorem le_of_mul_le_mul_left {α : Type u} [linear_ordered_semiring α] {a b c : α} (h : c * a ≤ c * b) (hc : 0 < c) :
a ≤ b
source
theorem le_of_mul_le_mul_right {α : Type u} [linear_ordered_semiring α] {a b c : α} (h : a * c ≤ b * c) (hc : 0 < c) :
a ≤ b
source
theorem pos_and_pos_or_neg_and_neg_of_mul_pos {α : Type u} [linear_ordered_semiring α] {a b : α} (hab : 0 < a * b) :
0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
source
theorem nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nnonneg {α : Type u} [linear_ordered_semiring α] {a b : α} (hab : 0 ≤ a * b) :
0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
source
theorem pos_of_mul_pos_left {α : Type u} [linear_ordered_semiring α] {a b : α} (h : 0 < a * b) (ha : 0 ≤ a) :
0 < b
source
theorem pos_of_mul_pos_right {α : Type u} [linear_ordered_semiring α] {a b : α} (h : 0 < a * b) (hb : 0 ≤ b) :
0 < a
source
theorem pos_iff_pos_of_mul_pos {α : Type u} [linear_ordered_semiring α] {a b : α} (hab : 0 < a * b) :
0 < a ↔ 0 < b
source
theorem neg_of_mul_pos_left {α : Type u} [linear_ordered_semiring α] {a b : α} (h : 0 < a * b) (ha : a ≤ 0) :
b < 0
source
theorem neg_of_mul_pos_right {α : Type u} [linear_ordered_semiring α] {a b : α} (h : 0 < a * b) (ha : b ≤ 0) :
a < 0
source
theorem neg_iff_neg_of_mul_pos {α : Type u} [linear_ordered_semiring α] {a b : α} (hab : 0 < a * b) :
a < 0 ↔ b < 0
source
@[simp]
theorem inv_of_pos {α : Type u} [linear_ordered_semiring α] {a : α} [invertible a] :
0 < ⅟ a ↔ 0 < a
source
@[simp]
theorem inv_of_nonpos {α : Type u} [linear_ordered_semiring α] {a : α} [invertible a] :
⅟ a ≤ 0 ↔ a ≤ 0
source
theorem nonneg_of_mul_nonneg_left {α : Type u} [linear_ordered_semiring α] {a b : α} (h : 0 ≤ a * b) (h1 : 0 < a) :
0 ≤ b
source
theorem nonneg_of_mul_nonneg_right {α : Type u} [linear_ordered_semiring α] {a b : α} (h : 0 ≤ a * b) (h1 : 0 < b) :
0 ≤ a
source
@[simp]
theorem inv_of_nonneg {α : Type u} [linear_ordered_semiring α] {a : α} [invertible a] :
0 ≤ ⅟ a ↔ 0 ≤ a
source
@[simp]
theorem inv_of_lt_zero {α : Type u} [linear_ordered_semiring α] {a : α} [invertible a] :
⅟ a < 0 ↔ a < 0
source
@[simp]
theorem inv_of_le_one {α : Type u} [linear_ordered_semiring α] {a : α} [invertible a] (h : 1 ≤ a) :
⅟ a ≤ 1
source
theorem neg_of_mul_neg_left {α : Type u} [linear_ordered_semiring α] {a b : α} (h : a * b < 0) (h1 : 0 ≤ a) :
b < 0
source
theorem neg_of_mul_neg_right {α : Type u} [linear_ordered_semiring α] {a b : α} (h : a * b < 0) (h1 : 0 ≤ b) :
a < 0
source
theorem nonpos_of_mul_nonpos_left {α : Type u} [linear_ordered_semiring α] {a b : α} (h : a * b ≤ 0) (h1 : 0 < a) :
b ≤ 0
source
theorem nonpos_of_mul_nonpos_right {α : Type u} [linear_ordered_semiring α] {a b : α} (h : a * b ≤ 0) (h1 : 0 < b) :
a ≤ 0
source
@[simp]
theorem mul_le_mul_left {α : Type u} [linear_ordered_semiring α] {a b c : α} (h : 0 < c) :
c * a ≤ c * b ↔ a ≤ b
source
@[simp]
theorem mul_le_mul_right {α : Type u} [linear_ordered_semiring α] {a b c : α} (h : 0 < c) :
a * c ≤ b * c ↔ a ≤ b
source
@[simp]
theorem mul_lt_mul_left {α : Type u} [linear_ordered_semiring α] {a b c : α} (h : 0 < c) :
c * a < c * b ↔ a < b
source
@[simp]
theorem mul_lt_mul_right {α : Type u} [linear_ordered_semiring α] {a b c : α} (h : 0 < c) :
a * c < b * c ↔ a < b
source
@[simp]
theorem zero_le_mul_left {α : Type u} [linear_ordered_semiring α] {b c : α} (h : 0 < c) :
0 ≤ c * b ↔ 0 ≤ b
source
@[simp]
theorem zero_le_mul_right {α : Type u} [linear_ordered_semiring α] {b c : α} (h : 0 < c) :
0 ≤ b * c ↔ 0 ≤ b
source
@[simp]
theorem zero_lt_mul_left {α : Type u} [linear_ordered_semiring α] {b c : α} (h : 0 < c) :
0 < c * b ↔ 0 < b
source
@[simp]
theorem zero_lt_mul_right {α : Type u} [linear_ordered_semiring α] {b c : α} (h : 0 < c) :
0 < b * c ↔ 0 < b
source
theorem add_le_mul_of_left_le_right {α : Type u} [linear_ordered_semiring α] {a b : α} (a2 : 2 ≤ a) (ab : a ≤ b) :
a + b ≤ a * b
source
theorem add_le_mul_of_right_le_left {α : Type u} [linear_ordered_semiring α] {a b : α} (b2 : 2 ≤ b) (ba : b ≤ a) :
a + b ≤ a * b
source
theorem add_le_mul {α : Type u} [linear_ordered_semiring α] {a b : α} (a2 : 2 ≤ a) (b2 : 2 ≤ b) :
a + b ≤ a * b
source
theorem add_le_mul' {α : Type u} [linear_ordered_semiring α] {a b : α} (a2 : 2 ≤ a) (b2 : 2 ≤ b) :
a + b ≤ b * a
source
@[simp]
theorem bit0_le_bit0 {α : Type u} [linear_ordered_semiring α] {a b : α} [nontrivial α] :
bit0 a ≤ bit0 b ↔ a ≤ b
source
@[simp]
theorem bit0_lt_bit0 {α : Type u} [linear_ordered_semiring α] {a b : α} [nontrivial α] :
bit0 a < bit0 b ↔ a < b
source
@[simp]
theorem bit1_le_bit1 {α : Type u} [linear_ordered_semiring α] {a b : α} [nontrivial α] :
bit1 a ≤ bit1 b ↔ a ≤ b
source
@[simp]
theorem bit1_lt_bit1 {α : Type u} [linear_ordered_semiring α] {a b : α} [nontrivial α] :
bit1 a < bit1 b ↔ a < b
source
@[simp]
theorem one_le_bit1 {α : Type u} [linear_ordered_semiring α] {a : α} [nontrivial α] :
1 ≤ bit1 a ↔ 0 ≤ a
source
@[simp]
theorem one_lt_bit1 {α : Type u} [linear_ordered_semiring α] {a : α} [nontrivial α] :
1 < bit1 a ↔ 0 < a
source
@[simp]
theorem zero_le_bit0 {α : Type u} [linear_ordered_semiring α] {a : α} [nontrivial α] :
0 ≤ bit0 a ↔ 0 ≤ a
source
@[simp]
theorem zero_lt_bit0 {α : Type u} [linear_ordered_semiring α] {a : α} [nontrivial α] :
0 < bit0 a ↔ 0 < a
source
theorem le_mul_iff_one_le_left {α : Type u} [linear_ordered_semiring α] {a b : α} (hb : 0 < b) :
b ≤ a * b ↔ 1 ≤ a
source
theorem lt_mul_iff_one_lt_left {α : Type u} [linear_ordered_semiring α] {a b : α} (hb : 0 < b) :
b < a * b ↔ 1 < a
source
theorem le_mul_iff_one_le_right {α : Type u} [linear_ordered_semiring α] {a b : α} (hb : 0 < b) :
b ≤ b * a ↔ 1 ≤ a
source
theorem lt_mul_iff_one_lt_right {α : Type u} [linear_ordered_semiring α] {a b : α} (hb : 0 < b) :
b < b * a ↔ 1 < a
source
theorem mul_nonneg_iff_right_nonneg_of_pos {α : Type u} [linear_ordered_semiring α] {a b : α} (ha : 0 < a) :
0 ≤ a * b ↔ 0 ≤ b
source
theorem mul_nonneg_iff_left_nonneg_of_pos {α : Type u} [linear_ordered_semiring α] {a b : α} (hb : 0 < b) :
0 ≤ a * b ↔ 0 ≤ a
source
theorem mul_le_iff_le_one_left {α : Type u} [linear_ordered_semiring α] {a b : α} (hb : 0 < b) :
a * b ≤ b ↔ a ≤ 1
source
theorem mul_lt_iff_lt_one_left {α : Type u} [linear_ordered_semiring α] {a b : α} (hb : 0 < b) :
a * b < b ↔ a < 1
source
theorem mul_le_iff_le_one_right {α : Type u} [linear_ordered_semiring α] {a b : α} (hb : 0 < b) :
b * a ≤ b ↔ a ≤ 1
source
theorem mul_lt_iff_lt_one_right {α : Type u} [linear_ordered_semiring α] {a b : α} (hb : 0 < b) :
b * a < b ↔ a < 1
source
theorem nonpos_of_mul_nonneg_left {α : Type u} [linear_ordered_semiring α] {a b : α} (h : 0 ≤ a * b) (hb : b < 0) :
a ≤ 0
source
theorem nonpos_of_mul_nonneg_right {α : Type u} [linear_ordered_semiring α] {a b : α} (h : 0 ≤ a * b) (ha : a < 0) :
b ≤ 0
source
@[protected, instance]
def linear_ordered_semiring.to_no_top_order {α : Type u_1} [linear_ordered_semiring α] :
no_top_order α
source
def function.injective.linear_ordered_semiring {α : Type u} [linear_ordered_semiring α] {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :
linear_ordered_semiring β

Pullback a linear_ordered_semiring under an injective map. See note [reducible non-instances].

Equations
source
theorem monotone_mul_left_of_nonneg {α : Type u} [linear_ordered_semiring α] {a : α} (ha : 0 ≤ a) :
monotone (λ (x : α), a * x)
source
theorem monotone_mul_right_of_nonneg {α : Type u} [linear_ordered_semiring α] {a : α} (ha : 0 ≤ a) :
monotone (λ (x : α), x * a)
source
theorem monotone.mul_const {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f : β → α} {a : α} (hf : monotone f) (ha : 0 ≤ a) :
monotone (λ (x : β), (f x) * a)
source
theorem monotone.const_mul {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f : β → α} {a : α} (hf : monotone f) (ha : 0 ≤ a) :
monotone (λ (x : β), a * f x)
source
theorem monotone.mul {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f g : β → α} (hf : monotone f) (hg : monotone g) (hf0 : ∀ (x : β), 0 ≤ f x) (hg0 : ∀ (x : β), 0 ≤ g x) :
monotone (λ (x : β), (f x) * g x)
source
theorem strict_mono_mul_left_of_pos {α : Type u} [linear_ordered_semiring α] {a : α} (ha : 0 < a) :
strict_mono (λ (x : α), a * x)
source
theorem strict_mono_mul_right_of_pos {α : Type u} [linear_ordered_semiring α] {a : α} (ha : 0 < a) :
strict_mono (λ (x : α), x * a)
source
theorem strict_mono.mul_const {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f : β → α} {a : α} (hf : strict_mono f) (ha : 0 < a) :
strict_mono (λ (x : β), (f x) * a)
source
theorem strict_mono.const_mul {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f : β → α} {a : α} (hf : strict_mono f) (ha : 0 < a) :
strict_mono (λ (x : β), a * f x)
source
theorem strict_mono.mul_monotone {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f g : β → α} (hf : strict_mono f) (hg : monotone g) (hf0 : ∀ (x : β), 0 ≤ f x) (hg0 : ∀ (x : β), 0 < g x) :
strict_mono (λ (x : β), (f x) * g x)
source
theorem monotone.mul_strict_mono {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f g : β → α} (hf : monotone f) (hg : strict_mono g) (hf0 : ∀ (x : β), 0 < f x) (hg0 : ∀ (x : β), 0 ≤ g x) :
strict_mono (λ (x : β), (f x) * g x)
source
theorem strict_mono.mul {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f g : β → α} (hf : strict_mono f) (hg : strict_mono g) (hf0 : ∀ (x : β), 0 ≤ f x) (hg0 : ∀ (x : β), 0 ≤ g x) :
strict_mono (λ (x : β), (f x) * g x)
source
theorem mul_max_of_nonneg {α : Type u} [linear_ordered_semiring α] {a : α} (b c : α) (ha : 0 ≤ a) :
a * max b c = max (a * b) (a * c)
source
theorem mul_min_of_nonneg {α : Type u} [linear_ordered_semiring α] {a : α} (b c : α) (ha : 0 ≤ a) :
a * min b c = min (a * b) (a * c)
source
theorem max_mul_of_nonneg {α : Type u} [linear_ordered_semiring α] {c : α} (a b : α) (hc : 0 ≤ c) :
(max a b) * c = max (a * c) (b * c)
source
theorem min_mul_of_nonneg {α : Type u} [linear_ordered_semiring α] {c : α} (a b : α) (hc : 0 ≤ c) :
(min a b) * c = min (a * c) (b * c)
source
@[instance]
def ordered_ring.to_ordered_add_comm_group (α : Type u) [self : ordered_ring α] :
ordered_add_comm_group α
source
@[class]
structure ordered_ring (α : Type u) :
Type u
  • add : α → α → α
  • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • nsmul : ℕ → α → α
  • nsmul_zero' : (∀ (x : α), ordered_ring.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ℕ) (x : α), ordered_ring.nsmul n.succ x = x + ordered_ring.nsmul n x) . "try_refl_tac"
  • neg : α → α
  • sub : α → α → α
  • sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
  • zsmul : ℤ → α → α
  • zsmul_zero' : (∀ (a : α), ordered_ring.zsmul 0 a = 0) . "try_refl_tac"
  • zsmul_succ' : (∀ (n : ℕ) (a : α), ordered_ring.zsmul (int.of_nat n.succ) a = a + ordered_ring.zsmul (int.of_nat n) a) . "try_refl_tac"
  • zsmul_neg' : (∀ (n : ℕ) (a : α), ordered_ring.zsmul -[1+ n] a = -ordered_ring.zsmul ↑(n.succ) a) . "try_refl_tac"
  • add_left_neg : ∀ (a : α), -a + a = 0
  • add_comm : ∀ (a b : α), a + b = b + a
  • mul : α → α → α
  • mul_assoc : ∀ (a b c : α), (a * b) * c = a * b * c
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • npow : ℕ → α → α
  • npow_zero' : (∀ (x : α), ordered_ring.npow 0 x = 1) . "try_refl_tac"
  • npow_succ' : (∀ (n : ℕ) (x : α), ordered_ring.npow n.succ x = x * ordered_ring.npow n x) . "try_refl_tac"
  • left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
  • right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
  • zero_le_one : 0 ≤ 1
  • mul_pos : ∀ (a b : α), 0 < a → 0 < b → 0 < a * b

An ordered_ring α is a ring α with a partial order such that addition is monotone and multiplication by a positive number is strictly monotone.

Instances
source
@[instance]
def ordered_ring.to_ring (α : Type u) [self : ordered_ring α] :
ring α
source
@[protected]
theorem decidable.ordered_ring.mul_nonneg {α : Type u} [ordered_ring α] [decidable_rel has_le.le] {a b : α} (h₁ : 0 ≤ a) (h₂ : 0 ≤ b) :
0 ≤ a * b
source
theorem ordered_ring.mul_nonneg {α : Type u} [ordered_ring α] {a b : α} :
0 ≤ a → 0 ≤ b → 0 ≤ a * b
source
@[protected]
theorem decidable.ordered_ring.mul_le_mul_of_nonneg_left {α : Type u} [ordered_ring α] {a b c : α} [decidable_rel has_le.le] (h₁ : a ≤ b) (h₂ : 0 ≤ c) :
c * a ≤ c * b
source
theorem ordered_ring.mul_le_mul_of_nonneg_left {α : Type u} [ordered_ring α] {a b c : α} :
a ≤ b → 0 ≤ c → c * a ≤ c * b
source
@[protected]
theorem decidable.ordered_ring.mul_le_mul_of_nonneg_right {α : Type u} [ordered_ring α] {a b c : α} [decidable_rel has_le.le] (h₁ : a ≤ b) (h₂ : 0 ≤ c) :
a * c ≤ b * c
source
theorem ordered_ring.mul_le_mul_of_nonneg_right {α : Type u} [ordered_ring α] {a b c : α} :
a ≤ b → 0 ≤ c → a * c ≤ b * c
source
theorem ordered_ring.mul_lt_mul_of_pos_left {α : Type u} [ordered_ring α] {a b c : α} (h₁ : a < b) (h₂ : 0 < c) :
c * a < c * b
source
theorem ordered_ring.mul_lt_mul_of_pos_right {α : Type u} [ordered_ring α] {a b c : α} (h₁ : a < b) (h₂ : 0 < c) :
a * c < b * c
source
@[protected, instance]
def ordered_ring.to_ordered_semiring {α : Type u} [ordered_ring α] :
ordered_semiring α
Equations
source
@[protected]
theorem decidable.mul_le_mul_of_nonpos_left {α : Type u} [ordered_ring α] [decidable_rel has_le.le] {a b c : α} (h : b ≤ a) (hc : c ≤ 0) :
c * a ≤ c * b
source
theorem mul_le_mul_of_nonpos_left {α : Type u} [ordered_ring α] {a b c : α} :
b ≤ a → c ≤ 0 → c * a ≤ c * b
source
@[protected]
theorem decidable.mul_le_mul_of_nonpos_right {α : Type u} [ordered_ring α] [decidable_rel has_le.le] {a b c : α} (h : b ≤ a) (hc : c ≤ 0) :
a * c ≤ b * c
source
theorem mul_le_mul_of_nonpos_right {α : Type u} [ordered_ring α] {a b c : α} :
b ≤ a → c ≤ 0 → a * c ≤ b * c
source
@[protected]
theorem decidable.mul_nonneg_of_nonpos_of_nonpos {α : Type u} [ordered_ring α] [decidable_rel has_le.le] {a b : α} (ha : a ≤ 0) (hb : b ≤ 0) :
0 ≤ a * b
source
theorem mul_nonneg_of_nonpos_of_nonpos {α : Type u} [ordered_ring α] {a b : α} :
a ≤ 0 → b ≤ 0 → 0 ≤ a * b
source
theorem mul_lt_mul_of_neg_left {α : Type u} [ordered_ring α] {a b c : α} (h : b < a) (hc : c < 0) :
c * a < c * b
source
theorem mul_lt_mul_of_neg_right {α : Type u} [ordered_ring α] {a b c : α} (h : b < a) (hc : c < 0) :
a * c < b * c
source
theorem mul_pos_of_neg_of_neg {α : Type u} [ordered_ring α] {a b : α} (ha : a < 0) (hb : b < 0) :
0 < a * b
source
def function.injective.ordered_ring {α : Type u} [ordered_ring α] {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) :
ordered_ring β

Pullback an ordered_ring under an injective map. See note [reducible non-instances].

Equations
source
theorem le_iff_exists_nonneg_add {α : Type u} [ordered_ring α] (a b : α) :
a ≤ b ↔ ∃ (c : α) (H : c ≥ 0), b = a + c
source
@[instance]
def ordered_comm_ring.to_comm_ring (α : Type u) [self : ordered_comm_ring α] :
comm_ring α
source
@[instance]
def ordered_comm_ring.to_ordered_ring (α : Type u) [self : ordered_comm_ring α] :
ordered_ring α
source
@[class]
structure ordered_comm_ring (α : Type u) :
Type u

An ordered_comm_ring α is a commutative ring α with a partial order such that addition is monotone and multiplication by a positive number is strictly monotone.

Instances
source
@[protected, instance]
def ordered_comm_ring.to_ordered_comm_semiring {α : Type u} [ordered_comm_ring α] :
ordered_comm_semiring α
Equations
source
def function.injective.ordered_comm_ring {α : Type u} [ordered_comm_ring α] {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) :
ordered_comm_ring β

Pullback an ordered_comm_ring under an injective map. See note [reducible non-instances].

Equations
source
@[instance]
def linear_ordered_ring.to_nontrivial (α : Type u) [self : linear_ordered_ring α] :
nontrivial α
source
@[instance]
def linear_ordered_ring.to_linear_order (α : Type u) [self : linear_ordered_ring α] :
linear_order α
source
@[class]
structure linear_ordered_ring (α : Type u) :
Type u

A linear_ordered_ring α is a ring α with a linear order such that addition is monotone and multiplication by a positive number is strictly monotone.

Instances
source
@[instance]
def linear_ordered_ring.to_ordered_ring (α : Type u) [self : linear_ordered_ring α] :
ordered_ring α
source
@[protected, instance]
def linear_ordered_ring.to_linear_ordered_add_comm_group {α : Type u} [s : linear_ordered_ring α] :
linear_ordered_add_comm_group α
Equations
source
@[protected, instance]
def linear_ordered_ring.to_linear_ordered_semiring {α : Type u} [linear_ordered_ring α] :
linear_ordered_semiring α
Equations
source
@[protected, instance]
def linear_ordered_ring.is_domain {α : Type u} [linear_ordered_ring α] :
is_domain α
source
@[simp]
theorem abs_one {α : Type u} [linear_ordered_ring α] :
|1| = 1
source
@[simp]
theorem abs_two {α : Type u} [linear_ordered_ring α] :
|2| = 2
source
theorem abs_mul {α : Type u} [linear_ordered_ring α] (a b : α) :
|a * b| = |a| * |b|
source
def abs_hom {α : Type u} [linear_ordered_ring α] :
monoid_with_zero_hom α α

abs as a monoid_with_zero_hom.

Equations
source
@[simp]
theorem abs_mul_abs_self {α : Type u} [linear_ordered_ring α] (a : α) :
|a| * |a| = a * a
source
@[simp]
theorem abs_mul_self {α : Type u} [linear_ordered_ring α] (a : α) :
|a * a| = a * a
source
theorem mul_pos_iff {α : Type u} [linear_ordered_ring α] {a b : α} :
0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
source
theorem mul_neg_iff {α : Type u} [linear_ordered_ring α] {a b : α} :
a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
source
theorem mul_nonneg_iff {α : Type u} [linear_ordered_ring α] {a b : α} :
0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
source
theorem mul_nonneg_of_three {α : Type u} [linear_ordered_ring α] (a b c : α) :
0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a

Out of three elements of a linear_ordered_ring, two must have the same sign.

source
theorem mul_nonpos_iff {α : Type u} [linear_ordered_ring α] {a b : α} :
a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
source
theorem mul_self_nonneg {α : Type u} [linear_ordered_ring α] (a : α) :
0 ≤ a * a
source
@[simp]
theorem neg_le_self_iff {α : Type u} [linear_ordered_ring α] {a : α} :
-a ≤ a ↔ 0 ≤ a
source
@[simp]
theorem neg_lt_self_iff {α : Type u} [linear_ordered_ring α] {a : α} :
-a < a ↔ 0 < a
source
@[simp]
theorem le_neg_self_iff {α : Type u} [linear_ordered_ring α] {a : α} :
a ≤ -a ↔ a ≤ 0
source
@[simp]
theorem lt_neg_self_iff {α : Type u} [linear_ordered_ring α] {a : α} :
a < -a ↔ a < 0
source
@[simp]
theorem abs_eq_self {α : Type u} [linear_ordered_ring α] {a : α} :
|a| = a ↔ 0 ≤ a
source
@[simp]
theorem abs_eq_neg_self {α : Type u} [linear_ordered_ring α] {a : α} :
|a| = -a ↔ a ≤ 0
source
theorem abs_cases {α : Type u} [linear_ordered_ring α] (a : α) :
|a| = a ∧ 0 ≤ a ∨ |a| = -a ∧ a < 0

For an element a of a linear ordered ring, either abs a = a and 0 ≤ a, or abs a = -a and a < 0. Use cases on this lemma to automate linarith in inequalities

source
theorem gt_of_mul_lt_mul_neg_left {α : Type u} [linear_ordered_ring α] {a b c : α} (h : c * a < c * b) (hc : c ≤ 0) :
b < a
source
theorem neg_one_lt_zero {α : Type u} [linear_ordered_ring α] :
-1 < 0
source
theorem le_of_mul_le_of_one_le {α : Type u} [linear_ordered_ring α] {a b c : α} (h : a * c ≤ b) (hb : 0 ≤ b) (hc : 1 ≤ c) :
a ≤ b
source
theorem nonneg_le_nonneg_of_sq_le_sq {α : Type u} [linear_ordered_ring α] {a b : α} (hb : 0 ≤ b) (h : a * a ≤ b * b) :
a ≤ b
source
theorem mul_self_le_mul_self_iff {α : Type u} [linear_ordered_ring α] {a b : α} (h1 : 0 ≤ a) (h2 : 0 ≤ b) :
a ≤ b ↔ a * a ≤ b * b
source
theorem mul_self_lt_mul_self_iff {α : Type u} [linear_ordered_ring α] {a b : α} (h1 : 0 ≤ a) (h2 : 0 ≤ b) :
a < b ↔ a * a < b * b
source
theorem mul_self_inj {α : Type u} [linear_ordered_ring α] {a b : α} (h1 : 0 ≤ a) (h2 : 0 ≤ b) :
a * a = b * b ↔ a = b
source
@[simp]
theorem mul_le_mul_left_of_neg {α : Type u} [linear_ordered_ring α] {a b c : α} (h : c < 0) :
c * a ≤ c * b ↔ b ≤ a
source
@[simp]
theorem mul_le_mul_right_of_neg {α : Type u} [linear_ordered_ring α] {a b c : α} (h : c < 0) :
a * c ≤ b * c ↔ b ≤ a
source
@[simp]
theorem mul_lt_mul_left_of_neg {α : Type u} [linear_ordered_ring α] {a b c : α} (h : c < 0) :
c * a < c * b ↔ b < a
source
@[simp]
theorem mul_lt_mul_right_of_neg {α : Type u} [linear_ordered_ring α] {a b c : α} (h : c < 0) :
a * c < b * c ↔ b < a
source
theorem sub_one_lt {α : Type u} [linear_ordered_ring α] (a : α) :
a - 1 < a
source
theorem mul_self_pos {α : Type u} [linear_ordered_ring α] {a : α} (ha : a ≠ 0) :
0 < a * a
source
theorem mul_self_le_mul_self_of_le_of_neg_le {α : Type u} [linear_ordered_ring α] {x y : α} (h₁ : x ≤ y) (h₂ : -x ≤ y) :
x * x ≤ y * y
source
theorem nonneg_of_mul_nonpos_left {α : Type u} [linear_ordered_ring α] {a b : α} (h : a * b ≤ 0) (hb : b < 0) :
0 ≤ a
source
theorem nonneg_of_mul_nonpos_right {α : Type u} [linear_ordered_ring α] {a b : α} (h : a * b ≤ 0) (ha : a < 0) :
0 ≤ b
source
theorem pos_of_mul_neg_left {α : Type u} [linear_ordered_ring α] {a b : α} (h : a * b < 0) (hb : b ≤ 0) :
0 < a
source
theorem pos_of_mul_neg_right {α : Type u} [linear_ordered_ring α] {a b : α} (h : a * b < 0) (ha : a ≤ 0) :
0 < b
source
theorem neg_iff_pos_of_mul_neg {α : Type u} [linear_ordered_ring α] {a b : α} (hab : a * b < 0) :
a < 0 ↔ 0 < b
source
theorem pos_iff_neg_of_mul_neg {α : Type u} [linear_ordered_ring α] {a b : α} (hab : a * b < 0) :
0 < a ↔ b < 0
source
theorem mul_self_add_mul_self_eq_zero {α : Type u} [linear_ordered_ring α] {x y : α} :
x * x + y * y = 0 ↔ x = 0 ∧ y = 0

The sum of two squares is zero iff both elements are zero.

source
theorem eq_zero_of_mul_self_add_mul_self_eq_zero {α : Type u} [linear_ordered_ring α] {a b : α} (h : a * a + b * b = 0) :
a = 0
source
theorem abs_eq_iff_mul_self_eq {α : Type u} [linear_ordered_ring α] {a b : α} :
|a| = |b| ↔ a * a = b * b
source
theorem abs_lt_iff_mul_self_lt {α : Type u} [linear_ordered_ring α] {a b : α} :
|a| < |b| ↔ a * a < b * b
source
theorem abs_le_iff_mul_self_le {α : Type u} [linear_ordered_ring α] {a b : α} :
|a| ≤ |b| ↔ a * a ≤ b * b
source
theorem abs_le_one_iff_mul_self_le_one {α : Type u} [linear_ordered_ring α] {a : α} :
|a| ≤ 1 ↔ a * a ≤ 1
source
def function.injective.linear_ordered_ring {α : Type u} [linear_ordered_ring α] {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) :
linear_ordered_ring β

Pullback a linear_ordered_ring under an injective map. See note [reducible non-instances].

Equations
source
@[class]
structure linear_ordered_comm_ring (α : Type u) :
Type u

A linear_ordered_comm_ring α is a commutative ring α with a linear order such that addition is monotone and multiplication by a positive number is strictly monotone.

Instances
source
@[instance]
def linear_ordered_comm_ring.to_linear_ordered_ring (α : Type u) [self : linear_ordered_comm_ring α] :
linear_ordered_ring α
source
@[instance]
def linear_ordered_comm_ring.to_comm_monoid (α : Type u) [self : linear_ordered_comm_ring α] :
comm_monoid α
source
@[protected, instance]
def linear_ordered_comm_ring.to_ordered_comm_ring {α : Type u} [d : linear_ordered_comm_ring α] :
ordered_comm_ring α
Equations
source
@[protected, instance]
def linear_ordered_comm_ring.to_linear_ordered_semiring {α : Type u} [d : linear_ordered_comm_ring α] :
linear_ordered_semiring α
Equations
source
theorem max_mul_mul_le_max_mul_max {α : Type u} [linear_ordered_comm_ring α] {a d : α} (b c : α) (ha : 0 ≤ a) (hd : 0 ≤ d) :
max (a * b) (d * c) ≤ (max a c) * max d b
source
theorem abs_sub_sq {α : Type u} [linear_ordered_comm_ring α] (a b : α) :
|a - b| * |a - b| = a * a + b * b - ((1 + 1) * a) * b
source
@[simp]
theorem abs_dvd {α : Type u} [ring α] [linear_order α] (a b : α) :
|a| ∣ b ↔ a ∣ b
source
theorem abs_dvd_self {α : Type u} [ring α] [linear_order α] (a : α) :
|a| ∣ a
source
@[simp]
theorem dvd_abs {α : Type u} [ring α] [linear_order α] (a b : α) :
a ∣ |b| ↔ a ∣ b
source
theorem self_dvd_abs {α : Type u} [ring α] [linear_order α] (a : α) :
a ∣ |a|
source
theorem abs_dvd_abs {α : Type u} [ring α] [linear_order α] (a b : α) :
|a| ∣ |b| ↔ a ∣ b
source
theorem even_abs {α : Type u} [ring α] [linear_order α] {a : α} :
even |a| ↔ even a
source
theorem odd_abs {α : Type u} [ring α] [linear_order α] {a : α} :
odd |a| ↔ odd a
source
def function.injective.linear_ordered_comm_ring {α : Type u} [linear_ordered_comm_ring α] {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) :
linear_ordered_comm_ring β

Pullback a linear_ordered_comm_ring under an injective map. See note [reducible non-instances].

Equations
source
def ring.positive_cone.to_positive_cone {α : Type u_1} [ring α] (self : ring.positive_cone α) :
add_comm_group.positive_cone α

Forget that a positive cone in a ring respects the multiplicative structure.

source
@[nolint]
structure ring.positive_cone (α : Type u_1) [ring α] :
Type u_1
  • nonneg : α → Prop
  • pos : α → Prop
  • pos_iff : (∀ (a : α), self.pos a ↔ self.nonneg a ∧ ¬self.nonneg (-a)) . "order_laws_tac"
  • zero_nonneg : self.nonneg 0
  • add_nonneg : ∀ {a b : α}, self.nonneg a → self.nonneg b → self.nonneg (a + b)
  • nonneg_antisymm : ∀ {a : α}, self.nonneg a → self.nonneg (-a) → a = 0
  • one_nonneg : self.nonneg 1
  • mul_pos : ∀ (a b : α), self.pos a → self.pos b → self.pos (a * b)

A positive cone in a ring consists of a positive cone in underlying add_comm_group, which contains 1 and such that the positive elements are closed under multiplication.

source
@[nolint]
structure ring.total_positive_cone (α : Type u_1) [ring α] :
Type u_1

A positive cone in a ring induces a linear order if 1 is a positive element.

source
def ring.total_positive_cone.to_total_positive_cone {α : Type u_1} [ring α] (self : ring.total_positive_cone α) :
add_comm_group.total_positive_cone α

Forget that a total_positive_cone in a ring respects the multiplicative structure.

source
def ring.total_positive_cone.to_positive_cone {α : Type u_1} [ring α] (self : ring.total_positive_cone α) :
ring.positive_cone α

Forget that a total_positive_cone in a ring is total.

source
def ordered_ring.mk_of_positive_cone {α : Type u_1} [ring α] (C : ring.positive_cone α) :
ordered_ring α

Construct an ordered_ring by designating a positive cone in an existing ring.

Equations
source
def linear_ordered_ring.mk_of_positive_cone {α : Type u_1} [ring α] (C : ring.total_positive_cone α) :
linear_ordered_ring α

Construct a linear_ordered_ring by designating a positive cone in an existing ring.

Equations
source
@[class]
structure canonically_ordered_comm_semiring (α : Type u_1) :
Type u_1

A canonically ordered commutative semiring is an ordered, commutative semiring in which a ≤ b iff there exists c with b = a + c. This is satisfied by the natural numbers, for example, but not the integers or other ordered groups.

Instances
source
@[instance]
def canonically_ordered_comm_semiring.to_comm_semiring (α : Type u_1) [self : canonically_ordered_comm_semiring α] :
comm_semiring α
source
@[instance]
def canonically_ordered_comm_semiring.to_canonically_ordered_add_monoid (α : Type u_1) [self : canonically_ordered_comm_semiring α] :
canonically_ordered_add_monoid α
source
@[protected, instance]
def canonically_ordered_comm_semiring.to_no_zero_divisors {α : Type u} [canonically_ordered_comm_semiring α] :
no_zero_divisors α
source
@[protected, instance]
def canonically_ordered_comm_semiring.to_covariant_mul_le {α : Type u} [canonically_ordered_comm_semiring α] :
covariant_class α α has_mul.mul has_le.le
source
theorem canonically_ordered_comm_semiring.zero_lt_one {α : Type u} [canonically_ordered_comm_semiring α] [nontrivial α] :
0 < 1

A version of zero_lt_one : 0 < 1 for a canonically_ordered_comm_semiring.

source
@[simp]
theorem canonically_ordered_comm_semiring.mul_pos {α : Type u} [canonically_ordered_comm_semiring α] {a b : α} :
0 < a * b ↔ 0 < a ∧ 0 < b
source
@[protected]
theorem add_le_cancellable.mul_tsub {α : Type u} [canonically_ordered_comm_semiring α] {a b c : α} [has_sub α] [has_ordered_sub α] [is_total α has_le.le] (h : add_le_cancellable (a * c)) :
a * (b - c) = a * b - a * c
source
@[protected]
theorem add_le_cancellable.tsub_mul {α : Type u} [canonically_ordered_comm_semiring α] {a b c : α} [has_sub α] [has_ordered_sub α] [is_total α has_le.le] (h : add_le_cancellable (b * c)) :
(a - b) * c = a * c - b * c
source
theorem mul_tsub {α : Type u} [canonically_ordered_comm_semiring α] [has_sub α] [has_ordered_sub α] [is_total α has_le.le] [contravariant_class α α has_add.add has_le.le] (a b c : α) :
a * (b - c) = a * b - a * c
source
theorem tsub_mul {α : Type u} [canonically_ordered_comm_semiring α] [has_sub α] [has_ordered_sub α] [is_total α has_le.le] [contravariant_class α α has_add.add has_le.le] (a b c : α) :
(a - b) * c = a * c - b * c

Structures involving * and 0 on with_top and with_bot #

The main results of this section are with_top.canonically_ordered_comm_semiring and with_bot.comm_monoid_with_zero.

source
@[protected, instance]
def with_top.nontrivial {α : Type u} [nonempty α] :
nontrivial (with_top α)
source
@[protected, instance]
def with_top.mul_zero_class {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] :
mul_zero_class (with_top α)
Equations
source
theorem with_top.mul_def {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] {a b : with_top α} :
a * b = ite (a = 0 ∨ b = 0) 0 (option.bind a (λ (a : α), option.bind b (λ (b : α), ↑a * b)))
source
@[simp]
theorem with_top.mul_top {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] {a : with_top α} (h : a ≠ 0) :
a * ⊤ = ⊤
source
@[simp]
theorem with_top.top_mul {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] {a : with_top α} (h : a ≠ 0) :
⊤ * a = ⊤
source
@[simp]
theorem with_top.top_mul_top {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] :
⊤ * ⊤ = ⊤
source
@[norm_cast]
theorem with_top.coe_mul {α : Type u} [decidable_eq α] [mul_zero_class α] {a b : α} :
↑a * b = (↑a) * ↑b
source
theorem with_top.mul_coe {α : Type u} [decidable_eq α] [mul_zero_class α] {b : α} (hb : b ≠ 0) {a : with_top α} :
a * ↑b = option.bind a (λ (a : α), ↑a * b)
source
@[simp]
theorem with_top.mul_eq_top_iff {α : Type u} [decidable_eq α] [mul_zero_class α] {a b : with_top α} :
a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0
source
theorem with_top.mul_lt_top {α : Type u} [decidable_eq α] [mul_zero_class α] [partial_order α] {a b : with_top α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
a * b < ⊤
source
@[protected, instance]
def with_top.mul_zero_one_class {α : Type u} [decidable_eq α] [mul_zero_one_class α] [nontrivial α] :
mul_zero_one_class (with_top α)

nontrivial α is needed here as otherwise we have 1 * ⊤ = ⊤ but also = 0 * ⊤ = 0.

Equations
source
@[protected, instance]
def with_top.no_zero_divisors {α : Type u} [decidable_eq α] [mul_zero_class α] [no_zero_divisors α] :
no_zero_divisors (with_top α)
source
@[protected, instance]
def with_top.semigroup_with_zero {α : Type u} [decidable_eq α] [semigroup_with_zero α] [no_zero_divisors α] :
semigroup_with_zero (with_top α)
Equations
source
@[protected, instance]
def with_top.monoid_with_zero {α : Type u} [decidable_eq α] [monoid_with_zero α] [no_zero_divisors α] [nontrivial α] :
monoid_with_zero (with_top α)
Equations
source
@[protected, instance]
def with_top.comm_monoid_with_zero {α : Type u} [decidable_eq α] [comm_monoid_with_zero α] [no_zero_divisors α] [nontrivial α] :
comm_monoid_with_zero (with_top α)
Equations
source
@[protected, instance]
def with_top.comm_semiring {α : Type u} [decidable_eq α] [canonically_ordered_comm_semiring α] [nontrivial α] :
comm_semiring (with_top α)

This instance requires canonically_ordered_comm_semiring as it is the smallest class that derives from both non_assoc_non_unital_semiring and canonically_ordered_add_monoid, both of which are required for distributivity.

Equations
source
@[protected, instance]
def with_top.canonically_ordered_comm_semiring {α : Type u} [decidable_eq α] [canonically_ordered_comm_semiring α] [nontrivial α] :
canonically_ordered_comm_semiring (with_top α)
Equations
source
@[protected, instance]
def with_bot.nontrivial {α : Type u} [nonempty α] :
nontrivial (with_bot α)
source
@[protected, instance]
def with_bot.mul_zero_class {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] :
mul_zero_class (with_bot α)
Equations
source
theorem with_bot.mul_def {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] {a b : with_bot α} :
a * b = ite (a = 0 ∨ b = 0) 0 (option.bind a (λ (a : α), option.bind b (λ (b : α), ↑a * b)))
source
@[simp]
theorem with_bot.mul_bot {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] {a : with_bot α} (h : a ≠ 0) :
a * ⊥ = ⊥
source
@[simp]
theorem with_bot.bot_mul {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] {a : with_bot α} (h : a ≠ 0) :
⊥ * a = ⊥
source
@[simp]
theorem with_bot.bot_mul_bot {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] :
⊥ * ⊥ = ⊥
source
@[norm_cast]
theorem with_bot.coe_mul {α : Type u} [decidable_eq α] [mul_zero_class α] {a b : α} :
↑a * b = (↑a) * ↑b
source
theorem with_bot.mul_coe {α : Type u} [decidable_eq α] [mul_zero_class α] {b : α} (hb : b ≠ 0) {a : with_bot α} :
a * ↑b = option.bind a (λ (a : α), ↑a * b)
source
@[simp]
theorem with_bot.mul_eq_bot_iff {α : Type u} [decidable_eq α] [mul_zero_class α] {a b : with_bot α} :
a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0
source
theorem with_bot.bot_lt_mul {α : Type u} [decidable_eq α] [mul_zero_class α] [partial_order α] {a b : with_bot α} (ha : ⊥ < a) (hb : ⊥ < b) :
⊥ < a * b
source
@[protected, instance]
def with_bot.mul_zero_one_class {α : Type u} [decidable_eq α] [mul_zero_one_class α] [nontrivial α] :
mul_zero_one_class (with_bot α)

nontrivial α is needed here as otherwise we have 1 * ⊥ = ⊥ but also = 0 * ⊥ = 0.

Equations
source
@[protected, instance]
def with_bot.no_zero_divisors {α : Type u} [decidable_eq α] [mul_zero_class α] [no_zero_divisors α] :
no_zero_divisors (with_bot α)
source
@[protected, instance]
def with_bot.semigroup_with_zero {α : Type u} [decidable_eq α] [semigroup_with_zero α] [no_zero_divisors α] :
semigroup_with_zero (with_bot α)
Equations
source
@[protected, instance]
def with_bot.monoid_with_zero {α : Type u} [decidable_eq α] [monoid_with_zero α] [no_zero_divisors α] [nontrivial α] :
monoid_with_zero (with_bot α)
Equations
source
@[protected, instance]
def with_bot.comm_monoid_with_zero {α : Type u} [decidable_eq α] [comm_monoid_with_zero α] [no_zero_divisors α] [nontrivial α] :
comm_monoid_with_zero (with_bot α)
Equations
source
@[protected, instance]
def with_bot.comm_semiring {α : Type u} [decidable_eq α] [canonically_ordered_comm_semiring α] [nontrivial α] :
comm_semiring (with_bot α)
Equations